Paper Info
Title
Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata
Abstract
Multiprocessing systems are capable of running multiple processes concurrently. By now such systems have established themselves as the defacto standard for operating systems. At the core of an operating system is the ability to execute programs and as such there must be a primitive for instantiating new processes - also programs are allowed to die/terminate. Operating systems may allow the executing programs to split (spawn) into more computational threads in order to let programs take advantage of concurrent execution as well. One of the most used modelling languages, Timed Automata, is based on multiple automata interacting thus they easily model the concurrent execution of programs. However, this language assumes a fixed size system in the sense that automata cannot be created at will but must be instantiated when the overall system is created. This is in contrast with the fact that developers are able to create threads when needed. In this paper we present our continued work to incorporate spawning of threads into U PPAAL SMC. Our modelling language, Dynamic Networks of Stochastic Hybrid Automata, is essentially Timed Automata extended with a spawning primitive and a tear-down primitive. The dynamic creation of threads has the side-effect that it is no longer possible to use ordinary logics to specify behaviours of individual threads - because the threads no longer have unique names. In this paper we propose an extension of Metric Temporal Logic with means for quantifying over the dynamically created threads. This makes it possible to zoom in on individual threads and specify requirements to their future behaviour. Furthermore, we present a monitoring procedure for the logic based on rewriting formulas. The presented modelling language and the specification language have been implemented in U PPAAL SMC version 4.1.18.
Year
DOI
Venue
2014
10.1109/ACSD.2014.21
Application of Concurrency to System Design
Keywords
DocType
Citations 
concurrency control,multi-threading,operating systems (computers),rewriting systems,specification languages,stochastic automata,temporal logic,uppaal smc version 4.1.18,behaviour specification,computational threads,concurrent execution,dynamic networks,modelling languages,monitoring procedure,multiprocessing systems,operating systems,quantified dynamic metric temporal logic,requirement specification,rewriting formulas,spawning primitive,specification language,stochastic hybrid automata,tear-down primitive,timed automata,dynamic systems,qdmtl,statistical model checking
Conference
1
PageRank 
References 
Authors
0.34
7
5
Name
Order
Citations
PageRank
Alexandre David1166776.52
Kim G. Larsen23922254.03
Axel Legay32982181.47
Guangyuan Li4567.19
Danny Bøgsted Poulsen530813.03