Paper Info
Title
Checking Critical Software Systems: A Formal Proposal
Abstract
As a contribution to the specification and verification of critical software systems, this article presents a formal proposal for compositional verification, which uses model checking technique and integrates a modelling infrastructure that propitiates the target system decomposition into separate components aimed at being individually specified and verified. Our goal with this proposal is to provide an infrastructure for developing and verifying critical software systems by fostering extensibility and modifiability of the software. In this way, validated components can be integrated into large computer programs readily. The compositional verification approach guarantees the correctness of the entire system during its execution. Also, is discussed a practical application of our proposal to a realistic industry project related to mobile phone communication.
Year
DOI
Venue
2016
10.1109/QUATIC.2016.041
2016 10th International Conference on the Quality of Information and Communications Technology (QUATIC)
Keywords
Field
DocType
Critical software systems,Safety-critical systems,Compositional verification,Model checking,Formal verification approach
Model checking,Systems engineering,Unified Modeling Language,Software engineering,Computer science,Correctness,Software system,Software,Software construction,Software verification and validation,Reliability engineering,Software verification
Conference
ISBN
Citations 
PageRank 
978-1-5090-3582-3
0
0.34
References 
Authors
5
2
Name
Order
Citations
PageRank
Luis E. Mendoza Morales1144.86
Manuel I. Capel25217.35