The practical applications of formal methods are increasing. This book contains the main proceedings of an international symposium on leveraging applications of formal methods (IsoLA). It consists of 12 papers.

The first introductory paper presents material required for understanding the issues in the next three papers. The paper looks at interaction and coordination in general, and the Extensible Markup Language (XML) data format and the dataflow-driven coordination language Reo in particular.

The second paper describes an application of the Reo coordination language. This language is used for modeling in systems biology. Reo is used to furnish a compositional formal model for outlining and arguing about the behavior of biological systems, such as regulatory gene networks. Reo allows the construction of connector circuits that have an exact formal semantics. Various forms of coordination in living cells are highlighted, and the metabolization of galactose is modeled. The authors claim that when Reo is used in systems biology, the consequence is a graphical model that is understandable, versatile, and mathematically accurate.

The third paper describes a tool for transforming structured data. A data transformation tool for XML, Rule Markup Language (RML), is introduced. RML can be used for rule-based transformations of XML documents. RML rules are stated in XML, and are meant to be combined with problem domain-specific XML, using XML wild-card elements. RML can be used to stipulate the semantics for statecharts and class diagrams in unified modeling language (UML) models.

The fourth paper describes the application of the tool mentioned in the previous paper, in the context of enterprise architectures. An enterprise architecture can be represented in an XML document. Using the RML tool, various views of this data can be found. The authors show that XML transformation techniques can be used to envision and examine enterprise architectures formally.

The fifth paper deals with the classification and utilization of abstractions for optimization. The authors propose that library-defined abstractions should be glossed with additional semantics in order to bolster their machine-driven optimization. They describe ROSE, a framework for building source-to-source translators that perform high-level optimizations on scientific applications.

The sixth paper is concerned with the correctness of transformations in compiler backends. Compiler backends transform intermediate languages into the code of the target machine. Backend generators permit the generation of compiler backends from a set of transformation rules. The authors study the correctness of these transformation rules.

The seventh paper focuses on accurate theorem proving for program verification. The authors suggest the use of a theorem prover called COGENT, which claims to provide better accuracy for ANSI-C expressions, with the potential for nested logic quantifiers. COGENT claims to help program verification tools conclude more incisively about finite machine-level variables, bit operations, structures, unions, references, pointers, and pointer arithmetic. The authors claim that the proposed approach is practical for industrial applications.

The eighth paper deals with designing safe and reliable systems using SCADE, a commercial product. SCADE permits the construction of formal models. SCADE Design Verifier is a tool within SCADE, which allows for the inclusion of faults using libraries of representative failures. The tool verifies whether systems remain safe when designated components fail. The paper includes examples from the aeronautics industry.

The ninth paper discusses ways of diminishing maintenance costs. This is done by introducing formal analysis of real-time behavior in industrial settings. The authors propose a framework for introducing the ability to analyze within a late phase of the system’s life cycle, using probabilistic formal models.

The tenth paper studies static timing analysis of real-time operating system code. Worst-case execution time (WCET) analysis helps to find an upper bound on the worst possible execution time of a computer program. Reliable WCET estimates are essential for designing and verifying real-time systems. The paper studies the difficulties in employing methods for WCET analysis.

The eleventh paper concentrates on domain-customized model checking for real-time component software. The authors describe a model-checking framework called Bogor. They report their experience in customizing Bogor to check design models of avionics systems (built using real-time common object request broker architecture (CORBA) component-based middleware).

The twelfth, and final, paper of the book looks at models for contract conformance. The authors claim to have implemented a contract checker for asynchronous message-passing applications (in order to check that service implementations conform to behavioral contracts). The goal of the paper is to explain the model construction, implemented by their contract checker, and its relation to a mathematical theory of conformance.

I find the papers highly informative; they exemplify ways to leverage applications of formal methods. I recommend that practitioners explore such applications.