Tehnički vjesnik, Vol. 30 No. 3, 2023.
Izvorni znanstveni članak
https://doi.org/10.17559/TV-20221025164232
Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence
Haihe Shi
; Jiangxi Normal University, School of Computer and Information Engineering, Nanchang, China
Sunwen Lan
; Jiangxi Normal University, School of Computer and Information Engineering, Nanchang, China
Riming Liu
; Jiangxi Normal University, School of Computer and Information Engineering, Nanchang, China
Haipeng Shi
; Jiangxi Normal University, School of Software, Nanchang, China
Sažetak
Pairwise sequence alignment is a classical problem in bioinformatics, aiming at finding the similarity between two sequences, which is important for discovering functional, structural and evolutionary information in biological sequences. More algorithms have been developed for the sequence alignment problem. There is no formal development process for the existing pairwise sequence algorithms and leads to the low trustworthiness of those algorithms. In addition, the application of formal methods in the field of bioinformatics algorithm development is rarely seen. In this paper, we use a formal method PAR to construct a pairwise sequence algorithm, analyze the essence of the pairwise sequence alignment problem, construct the Apla algorithm program by stepwise refinement, and further verify its correctness. Finally a highly reliable and executable pairwise sequence alignment algorithm program is generated from Apla program via PAR platform. The formal construction process ensures the reliability of algorithm, and also demonstrates the algorithm design idea clearly, which makes the originally difficult algorithm design process easier. The successful practice of this method on the pairwise sequence alignment problem in biological sequence analysis can provide a reference for the construction of highly reliable algorithms in complex bioinformatics from both methodological and practical aspects.
Ključne riječi
automatic verification; correctness by construction; pairwise sequence alignment; PAR method
Hrčak ID:
300681
URI
Datum izdavanja:
23.4.2023.
Posjeta: 485 *