A hierarchical verification approach to verify complex safety control systems based on STAMP

摘要

Complexity is a major obstacle to apply formal verification techniques in industry. Assume-guarantee (AG) reasoning is a promising compositional verification approach to deal with complexity. Proper decomposition and assumption design is vital in AG reasoning. We are motivated by the fact that a good insight into the target system can help the formal verification. So, instead of trying to automate the AG reasoning process, an accident model called STAMP is adopted to help us get a better understanding of the safety control system to be verified and a strategy for decomposition and designing assumptions accordingly. This conceptual approach is exemplified by verifying a simplified train control system. (C) 2018 Elsevier B.V. All rights reserved.