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

DOI10.1016/J.AMC.2012.02.018zbMath1252.68190OpenAlexW2064787495MaRDI QIDQ440685

Libero Nigro, Angelo Furfaro, Franco Cicirelli

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

modelingreal-time systemstimed automatamodel checkingschedulability analysis\texttt{UPPAAL}time stream Petri netstiming 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)

Uses Software

• TINA
• Uppaal

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Distributed simulation of modular time Petri nets: An approach and a case study exploiting temporal uncertainty
• Numerical computations and mathematical modelling with infinite and infinitesimal numbers
• A theory of timed automata
• Compact data structures and state-space reduction for model-checking real-time systems
• A new applied approach for executing computations with infinite and infinitesimal quantities
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Formal Methods for the Design of Real-Time Systems
• Lectures on Concurrency and Petri Nets

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