Verification of Distributed Artificial Intelligence Systems in Bioinformatics

TL;DR

This paper explores the use of model checking, a static analysis technique, to verify the correctness of distributed bioinformatics systems, emphasizing its importance for ensuring reliability in complex, concurrent software processes.

Contribution

It demonstrates the application and efficiency of model checking for verifying distributed bioinformatics systems with increasing concurrency, highlighting its significance in the field.

Findings

Model checking effectively verifies distributed bioinformatics processes.

Verification efficiency increases with process concurrency.

Experimental results align with theoretical expectations.

Abstract

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.