We now rely on computer software for everything from pacemakers and telephones to automobiles, airplanes, and spacecraft. Software is often the most expensive and least reliable component in the systems in which it is embedded. The construction and verification of software requires a range of expertise that is typically available only from a team of individuals and shared semantic models. Current technology for software development does not support such collaborative development.
This project is performing an exploratory study to design and prototype an open verification platform based on an evidential tool bus (ETB) for the integration of multiple logic-based tools. The Open Verification Platform (OVP) builds on the ETB to support the social construction of verified code for embedded software in cyber-physical systems. Such a platform would be used to synthesize the contributions of multiple sources of expertise in the verification of software, including domain experts, requirements analysts, developers, testers, and verification experts. The OVP design initiates a much-needed dialogue between researchers in cyber-physical systems (CPS) and verification tools to explore the architectural and semantic challenges in building collaborative tools. The project is using the OVP to bootstrap such a dialogue. The vision of the OVP effort is formal software development as a collaborative endeavor between diverse viewpoints and sources of expertise. It integrates formal verification tools within a social networking model so that problems can be solved quickly with the help of the appropriate experts. The broader impact of this proposal is in the design of a continuous social process for developing trustworthy cyber-physical systems, and for the rigorous training of software development teams.
As part of this effort, the project is organizing a workshop on Event-based Semantics to be held at CPSWEEK 2008, in St. Louis, Missouri. The shift towards openness, distribution of real time, embedded and critical systems, and the deep integration of software into physical systems, combined with the need for certification, results in a major verification challenge. The proposed workshop sets the stage for a new research area developing event-based models, logics, specification languages, and verification tools to support the design, development, maintenance, monitoring and evolution of cyber-physical systems and other distributed, real-time, embedded systems. The workshop seeks to develop broad agreement on the critical issues facing the modeling and design of distributed real-time systems in order to bridge the gap between the formal models and the urgent CPS engineering challenges.
