SGER: Open Verification Platform and Event-based Semantics

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