Automated V&V for high integrity systems, a targeted formal methods approach

摘要: This paper describes the intermediate results of a project to develop automated, high integrity, software verification and validation techniques for aerospace applications. Automated specification test case generation are made possible by targeted use formal methods. Specifically, restricted domain is exploited reduce set mathematical problems those that can be solved using constraint solvers, model checkers automated proof tactics. The practicality enhanced tight integration methods intuitive notations, existing modelling tools traditional development process. presents evidence support an emerging appreciation amongst engineering community that, benefits widely in industry, approach must taken integrates analysis with approaches powerful