Timed verification of the generic architecture of a memory circuit using parametric timed automata

DOI10.1007/s10703-008-0061-xzbMath1165.68401MaRDI QIDQ1028737

Laurent Fribourg, Weiwen Xu, Remy Chevallier, Emmanuelle Encrenaz-Tiphene

Publication date: 6 July 2009

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.545.7643

zbMATH Keywords

timed automata; model checking; memory circuit

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

What’s Decidable About Parametric Timed Automata?, Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*, Parametric Analyses of Attack-fault Trees*, Parametric metric interval temporal logic, Parameter synthesis for hierarchical concurrent real-time systems, \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability, Liveness of Parameterized Timed Networks, AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA

Uses Software

• Kronos
• Uppaal

Cites Work

• A theory of timed automata
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Verification of Asynchronous Circuits using Timed Automata
• Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata
• Static Analysis
• Formal Modeling and Analysis of Timed Systems