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.
翻译:此类项目包括空间探索、气象模型、基因组项目和其他许多项目。 关键是,协助这些项目的软件必须按预期去做。 在软件工程术语中,软件符合要求,即符合要求,即预期正确。 软件的正确性是软件工程领域大量研究的重点。 应用软件的实地从业者往往不重视检查这一正确性。 然而,随着软件系统变大,有可能与不同作者编写的分布式子系统相结合,这种核查就显得更加重要。 同时,分布式系统由于执行部件的速度不同,如僵局、种族条件或违反项目特性,容易出现危险的错误。该项目描述了一种静态分析方法的应用,称为模型检查,核查生物信息过程的分布式系统。在其中,我们评估了核查合并过程的模式方法的效率,同时执行的步骤越来越多,因此,这种核查工作变得更加重要。 同时,由于执行的系统执行速度不同,因此容易出现危险的错误,例如僵局、种族条件或违反项目特性。 这个项目描述了一种静态分析方法的应用,称为对生物信息学过程的分布式系统进行核查的模式检查。我们评价了核查方法对合并过程进行核查的效率,同时执行的合并步骤的次数越来越多,我们在分析中也显示了我们的实地试验结果。