A method for the automatic generation of test suites from object model - This paper explains how object models written in the Unified Modeling Language (UML) can be translated into formal, behavioural descriptions and used as a basis for automatic test generation. The behavioural descriptions are written in a language of communicating state machines: the Intermediate Format (IF). The translation from UML to IF is based upon an earlier formal semantics, written in the Abstract State Machine (ASM) notation. Descriptions written in IF can be automatically explored; the results of these explorations are test trees, ready for input to a variety of testing packages. Presented by Alessandra Cavarra, Charles Crichton and Jim Davies of Oxford University, UK at the Proceedings of the 2003 ACM symposium on Applied Computing.
ACM Digital Library - A searchable index of papers published in ACM journals. Queries are based on free-text searching in summaries of papers in the ACM publications database. Each summary contains title, author, journal, abstract, categories and subject descriptors from the ACM Computing Classification.
Building a Better Bug-trap - This is a general article setting formal methods in context. The article states, "People who write it are human first and programmers only second—in short, they make mistakes, lots of them. Can software help them write better software?" Published without an author listed in The Economist, Science Technology Quarterly>, 19 June 2003.
Formal Methods Europe FAQ: Formal Methods - FME is a European organization, supported by the Commission of the European Union, with the mission of promoting and supporting the industrial use of formal methods for computer systems development. This page, maintained by FME, responds to Frequently Asked Questions (FAQ) regarding Larch, Petri Nets, the Vienna Development Method (VDM) and Z notation for formal specification.
Petri Nets Bibliography - The Petri Net Bibliography contains all the references that were published in the Petri Nets Newsletter in previous years. The Petri Nets Newsletter is published by a German society for computer science.
Strategic Directions in Computing Research Formal Methods Working Group - Strategic Directions in Computing Research was funded by the Association for Computing Machinery with support from the National Science Foundation and the Office of Naval Research, and was cosponsored by the Computing Research Association. The meeting was hosted by the MIT Laboratory for Computer Science. The group report, Formal Methods: State of the Art and Future Directions, and links to members of the group are available on this page.
Survey of Formal Specification Techniques for Reactive Systems; An SEI Technical Report - This report develops a set of evaluation criteria and evaluates Communicating Sequential Processes (CSP), the Vienna Development Method (VDM), and temporal logic. The evaluation is based on specifications, written with each of the techniques, of an example avionics system. (CMU/SEI-90-TR-5)