Increasing the Practical Impact of Formal Methods for Computer-Aided SoftwareDevelopment

摘要

Current software development capabilities need improvement to effectively producesoftware that meets users' needs. Formal software models that can be mechanically processed can provide a sound basis for building and integrating tools that produce software faster, cheaper, and more reliably. Formal methods can also increase automation and decrease inconsistency in software development. The goal of the Monterey Workshop series is to help increase the practical impact of formal methods for software development so that these potential benefits can be realized in actual practice. Each year we focus in depth at one aspect of software development. In 1992, the focus was real-time and concurrent systems; in 1993, software slicing and merging; and in 1994, software evolution. This year's focus is specification-based software architectures. This workshop helps clarify what good formal methods are and what are their limits. According to Webster's Dictionary, formal means definite, orderly, and methodical; it does not necessarily entail logic or proofs or correctness. Everything that computers do is formal in the sense that syntactic structures are manipulated according to definite rules. Formal methods are syntactic in essence and semantic in purpose. Given the motivations of the workshop, we believe this is the most appropriate sense for the word 'formal' in the phrase formal methods. We expect the ultimate main benefits of formal methods to be decision support for and partial automation of the software development process.