Proving sequential function chart programs using timed automata

DOI10.1016/S0304-3975(00)00301-7MaRDI QIDQ5958730zbMATH OpenOpenAlexFDO

Authors D. L'Her, P. L. Parc, L. Marcé

Publication date 3 March 2002

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(00)00301-7

zbMATH Keywords

formal methodstimed automatacheckingsequential function chart (SFC)TCTL logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• Publication:4508304
• Automata and Logics for Timed Message Sequence Charts
• Verification of timed automata via satisfiability checking
• Timed semantics of message sequence charts based on timed automata
• Automatic Verification of Sequential Circuits Using Temporal Logic
• Temporal proof methodologies for timed transition systems
• The Power of Proofs: New Algorithms for Timed Automata Model Checking
• Timing diagrams: Formalization and algorithmic verification
• Automatic verification of timed concurrent constraint programs
• scientific article; zbMATH DE number 2087421

Cites work

• scientific article; zbMATH DE number 744075 (Why is no real title available?)
• Formal development of reactive systems. Case study production cell
• Symbolic model checking for real-time systems

Cited in

(3)

• scientific article; zbMATH DE number 1836375 (Why is no real title available?)
• Timed semantics of message sequence charts based on timed automata
• Modeling and proving Grafcets with transition systems

Describes a project that uses

Uses Software

• LUSTRE
• Kronos

This page was built for publication: Proving sequential function chart programs using timed automata

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