Software is a great enabler for a number of projects that otherwise would be impossible to perform. Such projects include Space Exploration, Weather Modeling, Genome Projects, and many others. It is critical that software aiding these projects does what it is expected to do. In the terminology of software engineering, software that corresponds to requirements, that is does what it is expected to do is called correct. Checking the correctness of software has been the focus of a great deal of research in the area of software engineering. Practitioners in the field in which software is applied quite often do not assign much value to checking this correctness. Yet, as software systems become larger, potentially combined with distributed subsystems written by different authors, such verification becomes even more important. Concurrent, distributed systems are prone to dangerous errors due to different speeds of execution of their components such as deadlocks, race conditions, or violation of project-specific properties. This project describes an application of a static analysis method called model checking to verification of a distributed system for the Bioinformatics process. In it, we evaluate the efficiency of the model checking approach to the verification of combined processes with an increasing number of concurrently executed steps. We show that our experimental results correspond to analytically derived expectations. We also highlight the importance of static analysis to combined processes in the Bioinformatics field.

翻译：软件是许多原本无法开展的项目的重要推动力，包括太空探索、天气建模、基因组项目等。确保辅助这些项目的软件能按预期运行至关重要。在软件工程术语中，符合需求即按预期运行的软件被称为正确的。验证软件的正确性一直是软件工程领域大量研究的焦点，但软件应用领域的实践者往往不重视这种正确性验证。然而，随着软件系统规模不断扩大，并可能集成不同开发者编写的分布式子系统，这种验证变得更加重要。并发分布式系统因其组件执行速度差异而易出现危险错误，如死锁、竞态条件或违反项目特定属性。本项目描述了一种名为模型检验的静态分析方法在生物信息学流程分布式系统验证中的应用。我们评估了模型检验方法对具有递增并发执行步骤的组合流程的验证效率，证明了实验结果与分析推导的预期结果相符，同时强调了静态分析对生物信息学领域组合流程的重要性。