Heterogeneous Specification Formalisms for 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''.