Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}

DOI10.1016/J.AMC.2012.02.018MaRDI QIDQ440685zbMATH OpenOpenAlexFDO

Authors Franco Cicirelli, Angelo Furfaro, Libero Nigro

Publication date 19 August 2012

Published in Applied Mathematics and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.amc.2012.02.018

zbMATH Keywords

\texttt{UPPAAL}model checkingmodelingreal-time systemsschedulability analysistime stream Petri netstimed automatatiming constraints

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

• Structural translation from time Petri nets to timed automata
• Specification and model checking of temporal properties in time Petri nets and timed automata
• TCTL model checking of time Petri nets
• Model checking of time Petri nets using the state class timed automaton
• scientific article; zbMATH DE number 1439078

Cites work

• A new applied approach for executing computations with infinite and infinitesimal quantities
• A theory of timed automata
• Compact data structures and state-space reduction for model-checking real-time systems
• Distributed simulation of modular time Petri nets: An approach and a case study exploiting temporal uncertainty
• Formal Methods for the Design of Real-Time Systems
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• Model-checking for probabilistic real-time systems
• Numerical computations and mathematical modelling with infinite and infinitesimal numbers
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Timed automata: Semantics, algorithms and tools

Cited in

(5)

• TAPAAL 2.0: integrated development environment for timed-arc Petri nets
• Towards building the state class graph of the TSPN model
• A time Petri net-based approach for synchronization, analysis and management of multimedia scenarios
• scientific article; zbMATH DE number 7333236 (Why is no real title available?)
• On-the-fly TCTL model checking for time Petri nets

Describes a project that uses

Uses Software

• Uppaal
• TINA

This page was built for publication: Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}

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