PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Banci M., Fantechi A., Gnesi S. Some experiences on formal specification of railway interlocking systems using statecharts. In: TRain Workshop at SEFM 2005 (Software Engineering and Formal Methods) (Koblenz - Germany, September 5-9, 2005).
 
 
Abstract
(English)
The introduction on the market of computerized Railway Interlocking Systems has pushed an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes and equipments for trains through a railway yard. Recently, a trend has emerged about the use of the graphical language statecharts as a standard formalism to produce precise specifications of these systems. This paper resumes our experiences in modeling railway interlocking systems using this formal language. Our studies have addressed the design problem from different points of view: we have modeled the specifications using two different approaches that we call functional description and geographical description. The names indicate that the first approach is focused on the modeling of the logical function of the Interlocking Systems, while the latter focuses on the geographical distributions of the element of the controlled station or yard. The geographical approach has also inspired a proposal for a distributed interlocking system, where the logical rules are embedded into distributed equipments communicating by means of safe buses.
Subject Railway signalling
Interlocking
Safety critical systems
Formal specification
D.2.1 Requirements/Specifications
D.2.2 Design Tools and Techniques
D.2.8 Metrics
J.7 Computers in Other Systems


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional