In recent years, researchers have recently developed a number of useful tools for automated analysis of particular classes of models of computer systems:
- Static analysis tools can analyze software source code, automatically constructing mathematical models of millions of pages length, proving non-interference of system components and detecting safety and security errors.
- Description logic reasoners analyze relationships between tens of thousands of terms in medical ontologies and verify their consistency.
- Hardware manufacturers are using SAT solvers, model checkers, and theorem provers to identify and correct subtle errors that could have enormous financial consequences.
- Software vendors are using static analyses supported by state-of-the art automated theorem provers and constraint solvers to prevent software crashes.
- Aircraft manufacturers and space agencies are using analysis tools based on abstract interpretation to eliminate errors in aircraft control software.
Despite these successes, today's automated analysis methods are not widespread in engineering practice, and therefore have a limited impact. One factor contributing to this state of affairs are the limitations of the tools themselves: the lack of automation, specialized input formats, and a limited use of high-level synthesis, which makes these tools expensive to use in practice. Another factor are the social circumstances, such as the lack of quality standards that would differentiate formally certified computer systems from systems without formal assurance guarantees.
To address these problems, the Action makes a conscious effort to unify current specialized algorithms and hide their internal complexity from the users. Among the central ideas in these activities is the notion of Rich Model, a precise and universal representation of different types of computer systems, different system aspects, and different levels of detail (from design to implementation, from functional correctness to timing and performance). Driven by this notion, the Action coordinates the development of automated analysis and synthesis tools, ensuring that the tools accept models expressed in the same general-purpose language, and enabling communication between the tools. Moreover, the Action coordinates research on concrete algorithms and tools for reasoning about the particular automated reasoning problems.
A number of national programs support research activities of the Action experts. Without the Action, however, these research activities would be carried out independently, would involve duplication of effort, and would not benefit from timely exchange of ideas. The strong need for coordination, as well as the fundamental and broad nature of the research involved means that no research program other than COST is appropriate to support such unified effort at this stage. The format of COST activities is ideal for the proposed coordination. The development of representation formats for rich models requires discussions of the parties involved, which is best done through joint COST meetings. The core technical work of the Action occurs in individual research groups, and short-term scientific missions for early-stage researchers are ideal for the necessary intense technical interaction.