System requirements and formal specifications of hierarchical reactive systems

Author

Togashi, Atsushi ; Lu, Xiaosong ; Kanezashi, Fumiaki

Author_Institution

Dept. of Comput. Sci., Shizuoka Univ., Hamamatsu, Japan

fYear

2000

fDate

2000

Firstpage

91

Lastpage

98

Abstract

A methodology for the description of system requirements and formal specifications of reactive systems and the synthesis of formal specifications is presented. Based on a hierarchical structure of system properties, a hierarchical assertion language is used as a requirement language and hierarchical state transition systems are used as formal specifications. Sound and complete formal specifications are synthesized from system requirements automatically. Modularity and reusability are supported by the introduction of requirement and specification modules and a partial order relation over these modules. The methodology has a practical significance because desired specifications of reactive systems can be derived or synthesized from user requirements on system functions in a systematic and stepwise way

Keywords

formal specification; real-time systems; software reusability; subroutines; completeness; formal specifications; hierarchical assertion language; hierarchical reactive systems; hierarchical state transition systems; modularity; partial order relation; requirement language; requirement modules; reusability; soundness; specification modules; system functions; system requirements; user requirements; Broadcasting; Computer science; Formal specifications; Prototypes; Reflection; Software prototyping;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Systems, 2000. Proceedings. Seventh International Conference on

Conference_Location

Iwate

ISSN

1521-9097

Print_ISBN

0-7695-0568-6

Type

conf

DOI

10.1109/ICPADS.2000.857687

Filename

857687