The presentation summarizes experiences in applying formal verification of software design artifacts using the SPIN model checker. The discussed example covers a crucial part of the firmware of the fault-tolerant programmable logic controller SIMATIC S7-400H. The presentation advocates the combination of formal verification of design artifacts with an appropriate test method applied on the software implementation. While formal verification complements the review process, testing benefits from the availability of correct formal models.
Target Audience: Software Engineers, Managers
Prerequisites: Experiences in software design and modeling languages; understanding of the V&V process
The development of a distributed system that comprises two or more components distributed over a network is challenging because of the inherent concurrency and need for coordination and synchronization. The problem is aggravated further if this system needs to fulfill stringent safety requirements. This presentation discusses an approach that is based on software behavior modeling and verifies the correctness of the model against the safety requirements. Afterwards this model is used to validate the correctness of the software implementation during testing. The approach is implemented using the open-source model-checker tool SPIN.
The presentation discusses the experiences in applying the outlined approach on a crucial part of the firmware of the fault-tolerant programmable logic controller Siemens SIMATIC S7-400H. It outlines the whole iterative process of model construction from available C code, model extension with new system features, model correctness checking using SPIN, validation of the C code implementation against the model via runtime verification during the testing phase. During the process design faults in the model and implementation faults in the running system are identified that would be hard to find using conventional methods of code review and testing.