Heterogeneous Specification Formalisms for Reactive Systems

Suny At Stony Brook, Stony Brook NY

Investigators

Abstract

Proposal Number: CCR-9988489 PI Name: Cleaveland, Walter R. Institution: SUNY at Stony Brook Title: Heterogeneous Specification Formalisms for Reactive Systems This project will investigate heterogeneous, mathematically rigorous modeling and analysis techniques for embedded software. The growing popularity of embedded computer controllers in devices ranging from airplanes to pacemakers to electric shavers points to the importance of cost-effective methods supporting the software they run. Traditional specification formalisms have emphasized homogeneous approaches in which all modeling and analysis occur within one framework, such as Statecharts or temporal logic; however, heterogeneous methodologies supporting multi-paradigm specifications have strong practical motivations, and informal design notations such as UML already provide superficial support for them. To enable heterogeneous systems specifications to be analyzed in a mathematically rigorous manner, thereby providing designers with feedback in advance of implementation, the project will pursue these lines of inquiry: the development of a uniform theory of operational and logic-based system specifications; the study of mechanisms for composing component models given in disparate formalisms; the implementation of automated tool support for verifying the correctness of heterogeneous specifications; and the investigation of case studies involving avionics systems and communication protocols. This research will enhance greatly the capabilities of formal system modeling and analysis by providing a rigorous basis for diverse embedded-software specification and verification technologies to ``interoperate''.