Formal parameters synthesis for track segments of a subway mesh
Adilson Luiz Bonifácio, A Moura, João Batista Camargo, Jorge Rady de Almeida · 2002
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.