SGER: Open Verification Platform and Event-based Semantics

从心脏起搏器、电话到汽车、飞机和宇宙飞船，我们现在的一切都依赖于计算机软件。软件通常是嵌入系统中最昂贵、最不可靠的组件。软件的构建和验证需要一系列的专业知识，这些专业知识通常只能从个人组成的团队和共享的语义模型中获得。当前的软件开发技术不支持这种协作开发。该项目正在进行一项探索性研究，以设计和原型一个基于证据工具总线（ETB）的开放式验证平台，用于集成多个基于逻辑的工具。开放式验证平台（Open Verification Platform， OVP）建立在ETB的基础上，支持网络物理系统中嵌入式软件验证码的社会化建设。这样一个平台将被用来综合软件验证中多种专业知识来源的贡献，包括领域专家、需求分析师、开发人员、测试人员和验证专家。OVP设计引发了网络物理系统（CPS）和验证工具研究人员之间急需的对话，以探索构建协作工具中的架构和语义挑战。该项目正在使用OVP来引导这样的对话。OVP工作的愿景是将正式的软件开发作为不同观点和专业知识来源之间的协作努力。它在社会网络模型中集成了正式的验证工具，以便在适当专家的帮助下快速解决问题。这一建议的更广泛的影响在于设计了一个持续的社会过程，用于开发值得信赖的网络物理系统，并对软件开发团队进行严格的培训。作为这项工作的一部分，该项目正在组织一个关于基于事件语义的研讨会，该研讨会将在密苏里州圣路易斯举行的CPSWEEK 2008上举行。向开放、实时、嵌入式和关键系统的分布以及软件与物理系统的深度集成的转变，加上对认证的需求，导致了一个重大的验证挑战。提议的研讨会为开发基于事件的模型、逻辑、规范语言和验证工具的新研究领域奠定了基础，以支持网络物理系统和其他分布式、实时嵌入式系统的设计、开发、维护、监控和演变。研讨会旨在就分布式实时系统建模和设计所面临的关键问题达成广泛的共识，以弥合正式模型与紧急CPS工程挑战之间的差距。

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.