Heterogeneous Specification Formalisms for Reactive Systems

提案号：CCR-9988489PI名称：克利夫兰，沃尔特r .机构：纽约州立大学石溪分校标题：反应系统的异构规范形式化该项目将研究嵌入式软件的异构，数学上严格的建模和分析技术。从飞机到起搏器再到电动剃须刀，嵌入式计算机控制器在各种设备中越来越受欢迎，这表明了支持它们运行的软件的成本效益方法的重要性。传统的规范形式化强调同构方法，其中所有建模和分析都发生在一个框架内，例如状态图或时间逻辑；然而，支持多范式规范的异构方法具有强大的实际动机，并且非正式的设计符号（如uml）已经为它们提供了表面的支持。为了使异构系统规范能够以数学上严格的方式进行分析，从而在实施之前为设计师提供反馈，该项目将追求以下探究方向：开发统一的基于操作和逻辑的系统规范理论；不同形式下组件模型组成机制的研究实现自动化工具支持验证异构规范的正确性；以及对涉及航空电子系统和通信协议的案例研究的调查。本研究将为各种嵌入式软件规范和验证技术的“互操作”提供严格的基础，从而极大地增强形式化系统建模和分析的能力。

Proposal Number: CCR-9988489PI Name: Cleaveland, Walter R.Institution: SUNY at Stony BrookTitle: Heterogeneous Specification Formalisms for Reactive SystemsThis project will investigate heterogeneous, mathematically rigorous modelingand analysis techniques for embedded software. The growing popularity ofembedded computer controllers in devices ranging from airplanes to pacemakers to electric shavers points to the importance of cost-effectivemethods supporting the software they run. Traditional specificationformalisms have emphasized homogeneous approaches in which all modeling andanalysis occur within one framework, such as Statecharts or temporal logic;however, heterogeneous methodologies supporting multi-paradigm specificationshave strong practical motivations, and informal design notations such as UMLalready provide superficial support for them. To enable heterogeneous systemsspecifications to be analyzed in a mathematically rigorous manner, therebyproviding designers with feedback in advance of implementation, the projectwill pursue these lines of inquiry: the development of a uniform theory ofoperational and logic-based system specifications; the study of mechanisms forcomposing component models given in disparate formalisms; the implementationof automated tool support for verifying the correctness of heterogeneousspecifications; and the investigation of case studies involving avionicssystems and communication protocols. This research will enhance greatly thecapabilities of formal system modeling and analysis by providing a rigorousbasis for diverse embedded-software specification and verificationtechnologies to ``interoperate''.