Formal parameters synthesis for track segments of a subway mesh

Author

Bonifácio, Adilson L. ; Moura, Arnaldo V. ; Camargo, João B., Jr. ; Almeida Junior, J.R.

Author_Institution

Inst. of Comput., Univ. Estadual de Campinas, Sao Paulo, Brazil

fYear

2000

fDate

2000

Firstpage

263

Lastpage

271

Abstract

The aim of this work is to apply formal specification techniques to model real-time distributed systems arising from real-world applications. The formal models discussed here are based on the notion of hybrid automata. The target system is the maneuvering yard of a subway mesh. Semi-automatic tools are used in the analysis and verification of the models here developed. The models are also used to synthesize some important parameters of the system wider consideration. All results were obtained on a typical 350 MHz desktop PC, with 320 MB of main memory

Keywords

automata theory; formal specification; formal verification; real-time systems; software metrics; formal models; formal parameters synthesis; formal specification; hybrid automata; real-time distributed systems; semi-automatic tools; subway mesh; track segments; verification; Automata; Character generation; Control systems; Control theory; Formal specifications; Read only memory; Real time systems; Topology;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Computer Based Systems, 2000. (ECBS 2000) Proceedings. Seventh IEEE International Conference and Workshopon the

Conference_Location

Edinburgh

Print_ISBN

0-7695-0604-6

Type

conf

DOI

10.1109/ECBS.2000.839885

Filename

839885