Heterogeneous Specification Formalisms for Reactive Systems

反应式系统的异构规范形式

• 批准号: 9988489
• 负责人: W. Rance Cleaveland
• 金额: $ 32.5万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2000
• 资助国家: 美国
• 起止时间: 2000-05-01 至 2005-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9988489&HistoricalAwards=false
• 关键词: Heterogeneous; Specification; Formalisms; Reactive; Systems

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''.

提案编号：CCR-9988489 PI名称： Cleaveland，Walter R.机构： SUNY at Stony BrookTitle： 反应式系统的异质规格说明形式本计画将研究异质的、数学上严格的嵌入式软体建模与分析技术。 嵌入式计算机控制器在从飞机到心脏起搏器到电动剃须刀的设备中越来越受欢迎，这表明了支持它们运行的软件的成本效益方法的重要性。 传统的规范形式主义强调所有建模和分析都发生在一个框架内的同质方法，如Statecharts或时态逻辑;然而，支持多范式规范的异构方法具有强大的实际动机，非正式的设计符号，如UML已经为它们提供了肤浅的支持。 为了使异构系统规范能够以数学上严格的方式进行分析，从而在实现之前为设计人员提供反馈，该项目追求以下调查路线：开发基于操作和逻辑的系统规范的统一理论;研究组成不同形式化的组件模型的机制;自动化工具支持的实现，用于验证异构规范的正确性;以及涉及航空电子系统和通信协议的案例研究的调查。 本文的研究将大大提高形式化系统建模和分析的能力，为各种嵌入式软件规范和验证技术的“互操作”提供严格的基础。