Verifying RTECTL properties of a train controller systems

MaRDI QIDQ5407112zbMATH OpenFDO

Authors Bożena Woźna-Szcześniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny

Publication date 4 April 2014

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Traffic problems in operations research (90B20)

Recommendations

• Comparing SAT- and SMT- based bounded model checking for ECTL properties
• SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking
• Verification of a controller for BART: An approach based on Horn logic and denotational semantics
• scientific article; zbMATH DE number 177509

Cited in

(3)

• Formal verification of safety protocol in train control system
• Using SCR to specify requirements of the BART advanced automated train control system
• Verification of a controller for BART: An approach based on Horn logic and denotational semantics

This page was built for publication: Verifying RTECTL properties of a train controller systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5407112)