Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence
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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Faculty of Mechanical Engineering in Slavonski Brod, Faculty of Electrical Engineering in Osijek, Faculty of Civil Engineering in Osijek
2023-01-01
|
| Series: | Tehnički Vjesnik |
| Subjects: | |
| Online Access: | https://hrcak.srce.hr/file/433787 |
| _version_ | 1797206524370616320 |
|---|---|
| author | Haihe Shi Sunwen Lan Riming Liu Haipeng Shi |
| author_facet | Haihe Shi Sunwen Lan Riming Liu Haipeng Shi |
| author_sort | Haihe Shi |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-24T09:08:23Z |
| format | Article |
| id | doaj.art-87ee45c2064845d6bd1e643abfa30e6d |
| institution | Directory Open Access Journal |
| issn | 1330-3651 1848-6339 |
| language | English |
| last_indexed | 2024-04-24T09:08:23Z |
| publishDate | 2023-01-01 |
| publisher | Faculty of Mechanical Engineering in Slavonski Brod, Faculty of Electrical Engineering in Osijek, Faculty of Civil Engineering in Osijek |
| record_format | Article |
| series | Tehnički Vjesnik |
| spelling | doaj.art-87ee45c2064845d6bd1e643abfa30e6d2024-04-15T18:25:32ZengFaculty of Mechanical Engineering in Slavonski Brod, Faculty of Electrical Engineering in Osijek, Faculty of Civil Engineering in OsijekTehnički Vjesnik1330-36511848-63392023-01-0130374274910.17559/TV-20221025164232Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-SequenceHaihe Shi0Sunwen Lan1Riming Liu2Haipeng Shi3Jiangxi Normal University, School of Computer and Information Engineering, Nanchang, ChinaJiangxi Normal University, School of Computer and Information Engineering, Nanchang, ChinaJiangxi Normal University, School of Computer and Information Engineering, Nanchang, ChinaJiangxi Normal University, School of Software, Nanchang, ChinaPairwise 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.https://hrcak.srce.hr/file/433787automatic verificationcorrectness by constructionpairwise sequence alignmentPAR method |
| spellingShingle | Haihe Shi Sunwen Lan Riming Liu Haipeng Shi Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence Tehnički Vjesnik automatic verification correctness by construction pairwise sequence alignment PAR method |
| title | Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence |
| title_full | Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence |
| title_fullStr | Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence |
| title_full_unstemmed | Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence |
| title_short | Correctness by Construction for Pairwise Sequence Alignment Algorithm in Bio-Sequence |
| title_sort | correctness by construction for pairwise sequence alignment algorithm in bio sequence |
| topic | automatic verification correctness by construction pairwise sequence alignment PAR method |
| url | https://hrcak.srce.hr/file/433787 |
| work_keys_str_mv | AT haiheshi correctnessbyconstructionforpairwisesequencealignmentalgorithminbiosequence AT sunwenlan correctnessbyconstructionforpairwisesequencealignmentalgorithminbiosequence AT rimingliu correctnessbyconstructionforpairwisesequencealignmentalgorithminbiosequence AT haipengshi correctnessbyconstructionforpairwisesequencealignmentalgorithminbiosequence |