Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller

dc.creatorSteggles,L.
dc.date2000
dc.date.accessioned2024-02-06T12:50:33Z
dc.date.available2024-02-06T12:50:33Z
dc.descriptionSecond-order algebraic methods provide a natural and expressive formal framework in which to develop correct computing systems. In this paper we consider using second-order algebraic methods to specify real-time systems and to verify their associated safety and utility properties. We demonstrate our ideas by presenting a detailed case study of the railroad crossing controller, a benchmark example in the real-time systems community. This case study demonstrates how real-time constraints can be modelled naturally using second-order algebras and illustrates the substantial expressive power of second-order equations.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-006-04-0460
dc.identifierhttps://lib.jucs.org/article/27673/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/7745
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 6(4): 460-473
dc.subjectreal-time systems
dc.subjectalgebraic specification methods
dc.subjectformal verification
dc.titleSpecifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller
dc.typeResearch Article
Файлы
Коллекции