Parametric model-checking of stopwatch Petri nets

MaRDI QIDQ4929342zbMATH OpenFDO

Authors Louis-Marie Traonouez, Didier Lime, Olivier H. Roux

Publication date 22 September 2010

Full work available at URL http://www.jucs.org/jucs_15_17/parametric_model_checking_of

zbMATH Keywords

parametersmodel-checkingstate-class graphtime Petri netsstopwatches

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
• Cost problems for parametric time Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets
• Bounded parametric verification for distributed time Petri nets with discrete-time semantics
• scientific article; zbMATH DE number 6708300

Cited in

(22)

• On-the-fly \(TCTL\) model checking for time Petri nets
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• Bounded parametric verification for distributed time Petri nets with discrete-time semantics
• Expressiveness of Petri Nets with Stopwatches. Dense-time Part
• FAST verification of the class of stop-and-wait protocols modelled by coloured Petri nets
• Cost problems for parametric time Petri nets
• \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability
• Parametric verification: an introduction
• Parametric model checking with VerICS
• Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets
• Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation
• Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
• Parameter synthesis for hierarchical concurrent real-time systems
• Shrinking of time Petri nets
• Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
• Parametric schedulability analysis of a launcher flight control system under reactivity constraints
• Formalising concurrent UML state machines using coloured Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets
• Parametric Language Analysis of the Class of Stop-and-Wait Protocols
• Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
• Symbolic unfolding of parametric stopwatch Petri nets
• scientific article; zbMATH DE number 7566044 (Why is no real title available?)

Describes a project that uses

Uses Software

• HyTech

This page was built for publication: Parametric model-checking of stopwatch Petri nets

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