Using formal verification techniques for dependability studies

摘要

This paper deals with the relationships between behavioural modeling and formal verification on one sie, and dependability analysis on the other side. We sketch an experiment carried out with an efficient formal model checker which was applied to the safety analysis of a computer controlled landing system. We discuss the needs for a closer integration between dysfunctional behavioural analysis and probabilistic analysis. We propose sequential Boolean circuits as a well defined and extensively investigated generalization of fault trees. We sketch some future work aming at overcoming the performance limitations of Markov analytic resolution or sequences' probability computation thanks to Binary Decision Diagrams (BDDs) algorithms. We point to the available theoretical results that will give a foundation framework for this algorithmic research.