Triumphs and Challenges for the Industrial Application of Model-Oriented Formal Methods Technical rept. series

摘要

The lightweight formal methods paradigm emphasises the use of abstract modelling as an aid to understanding and design of computer-based systems. It advocates careful targeting of formal methods technology on specific system parts or aspects, rather than large-scale application. The challenge of implementing the lightweight paradigm was taken up a decade ago by the community working with the Vienna Development Method (VDM), developing its semantics, tools and encouraging industry application. This paper reports industrial successes over that period, and identifies challenges for industrial formal methods application in the near future. This paper is to appear in the proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006).