Initial State Modeling of Interlocking System Using Maude

Autor:	Zhongwei Xu, Zuxi Chen, Rui Ma, Shuqing Zhang
Rok vydání:	2013
Předmět:	Model checking Test line Computer science Programming language Formal specification State (computer science) Rewriting Equational logic computer.software_genre Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION Formal verification computer Interlocking
Zdroj:	Lecture Notes in Electrical Engineering ISBN: 9783319017655
DOI:	10.1007/978-3-319-01766-2_36
Popis:	In order to do formal verification of interlocking system, which is complicated but safety critical, we choose formal specification language Maude for modeling and verification based on membership equational logic and rewriting logic. In this chapter, a method is proposed to show how the initial state can be modeled and contains important information of specific interlocking system. And a case of Tongji Test Line is reported to illustrate this method in detail. The verification results show that Maude can be applied to formal object-oriented specification and model checking of railway interlocking system successfully using the proposed modeling method.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::3f896aa8b3136bf22ffa1855e76f54a9 https://doi.org/10.1007/978-3-319-01766-2_36 Zobrazit plný text záznamu