Ensuring the correctness of critical real-time systems, involving concurrent behaviours and timing requirements, is crucial. Timed automata extend finite-state automata with clocks, compared in guards and invariants with integer constants. Parametric timed automata (PTAs) extend timed automata with timing parameters. Parameter synthesis aims at computing dense sets of valuations for the timing parameters, guaranteeing a good behaviour. However, in most cases, the emptiness problem for reachability (i.e., the emptiness of the parameter valuations set for which some location is reachable) is undecidable for PTAs and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproximation in the form of symbolic sets of valuations containing not only all the integer points ensuring reachability, but also all the (non-necessarily integer) convex combinations of these integer points, for general PTAs with a bounded parameter domain. We also propose two further algorithms synthesizing parameter valuations guaranteeing unavoidability, and preservation of the untimed behaviour w.r.t. a reference parameter valuation, respectively. Our algorithms terminate and can output sets of valuations arbitrarily close to the complete result. We demonstrate their applicability and efficiency using the tools Roméo and IMITATOR on several benchmarks.

The control of real-time systems often requires taking into account simultaneous access in true parallelism to shared resources. This is particularly the case for multicore execution platforms. Timed automata or time Petri nets do not capture these features directly. We first define High-level Colored Time Petri Net (HCTPN) that extends time Petri Nets with color and high-level functionality encompassing both timed multi-enableness of transitions and sequential pseudo code. We then extend HCTPN with stopwatches to allow the modeling of preemptive scheduling, which is an important feature in the real-time context. We prove that the reachability problem is decidable for HCTPN but is undecidable for HCTPN with stopwatches, and we propose an abstraction of the state space for these models. We apply this approach to model a preemptive multi-core real-time application that uses a spinlock mechanism in order to check all possible execution paths, interleaving of service calls, and preemptive scheduling.

The control of real-time systems often requires taking into account simultaneous access in true parallelism to shared resources. This is particularly the case for multi-core execution platforms. Timed automata or time Petri nets do not capture these features directly. We propose extending time Petri Nets with color and high-level functionality encompassing both timed multi-enableness of transitions and sequential pseudo code. We prove that the reachability problem is decidable for this model on which an on-the-fly TCTL model checking algorithm is efficiently implemented in the tool ROMEO. We apply this approach to modeling a multi-core real time spinlock mechanism in order to check all possible execution paths and interleaving of service calls.

We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interesting problems are undecidable. Notably, the parametric reachability emptiness problem, i.e., the emptiness of the parameter valuations set allowing to reach some given discrete state, is undecidable. Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve decidability for reachability properties by enforcing a separation of parameters used as upper bounds in the automaton constraints, and those used as lower bounds. In this paper, we first study reachability. We exhibit a subclass of PTAs (namely integer-points PTAs) with bounded rational-valued parameters for which the parametric reachability emptiness problem is decidable. Using this class, we present further results improving the boundary between decidability and undecidability for PTAs and their subclasses such as L/U-PTAs. We then study liveness. We prove that: (1) deciding the existence of at least one parameter valuation for which there exists an infinite run in an L/U-PTA is PSpace-complete; (2) the existence of a parameter valuation such that the system has a deadlock is however undecidable; (3) the problem of the existence of a valuation for which a run remains in a given set of locations exhibits a very thin border between decidability and undecidability.

A major step in arithmetic operators design is the placement of pipeline stages, with the goal of drastically increase the data throughput. Approaches, such as the as-soon-as-possible greedy algorithm, allow pipelining with a frequency target. They can possibly be combined with a retiming operation to reduce the number of pipeline registers. This retiming step is based on a weighted directed graph model, from which the pipeline placement is reduced to an optimisation problem (for example ILP). However, this approach produces only a unique solution, and makes it difficult to add additional constraints on the resulting pipeline. We propose to use a Timed Petri Net extension with cost, where time captures the propagation delay and cost measures the size of pipeline registers. The state space of the model captures exactly the circuit states and the branching points, so its exploration can be guided by comparing the circuit states regarding any feature (number and size of registers, critical path, throughput, etc). The pipeline exploration can be reduced to a weighted branching-time logic model-checking problem, that we prove to be PSPACE-complete on this model. We have implemented this exploration algorithm in a prototype tool. We apply it on some arithmetic operators provided by FloPoCo showing improvements up to 35% compared to the current implementation.

We investigate the problem of parameter synthesis for time Petri nets with a cost variable that evolves both continuously with time, and discretely when firing transitions. More precisely, parameters are rational symbolic constants used for time constraints on the firing of transitions and we want to synthesise all their values such that some marking is reachable, with a cost that is either minimal or simply less than a given bound. We first prove that the mere existence of values for the parameters such that the latter property holds is undecidable. We nonetheless provide symbolic semi-algorithms for the two synthesis problems and we prove them both sound and complete when they terminate. We also show how to modify them for the case when parameter values are integers. Finally, we prove that these modified versions terminate if parameters are bounded. While this is to be expected since there are now only a finite number of possible parameter values, our algorithms are symbolic and thus avoid an explicit enumeration of all those values. Furthermore, the results are symbolic constraints representing finite unions of convex polyhedra that are easily amenable to further analysis through linear programming. We finally report on the implementation of the approach in Romeo, a software tool for the analysis of time Petri nets.

This special issue is based on extended versions of the best papers presented at the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2018).Petri Nets 2018 was co-located with the Application of Concurrency to System Design Conference (ACSD 2018).Both were organized by the Interes Institute and Faculty of Electrical Engineering and Information Technology, Slovak University of Technology.The conference took place at the Austria Trend Hotel Bratislava, from June 24 to June 29, 2018.In total, 33 papers were submitted to Petri Nets 2018 by authors from 19 different countries.Each paper was reviewed by three reviewers.The Program Committee (PC) selected 23 papers for presentation: 15 theory papers and 8 tool papers.The authors of the best six papers were invited to submit an extended version of their conference paper for this special issue.The selected papers contained highly innovative and very strong contributions, as was demonstrated by the unanimous support of the reviewers.Also the PC unanimously supported these invitations.After a rigorous review process comprising two rounds of reviewing, the invited papers were accepted.Besides a subset of the original reviewers, we also invited additional reviewers to ensure the best feedback possible.We believe that the papers in this special issue are of high quality and represent the state-of-the-art in their respective fields.The article "Analysis and Synthesis of Weighted Marked Graph Petri Nets" by Raymond Devillers and Thomas Hujsa focuses on an important subclass of persistent Petri nets, the weighted marked graphs (WMGs), also called generalised (or weighted) event (or marked) graphs or weighted T-nets.The authors provide new behavioural properties of WMGs expressed on their reachability graph, notably backward persistence and strong similarities between any two sequences sharing the same starting state and the same destination state.They also propose necessary structural conditions that must be fulfilled by a labelled transition system to be WMG-solvable.Finally, the authors propose a general synthesis method to create a WMG whose reachability graph minimally includes the specification.The article "Operational Semantics, Interval Orders and Sequences of Antichains" by Ryszard Janicki and Maciej Koutny introduces a new general class of nets that can represent both inhibitor and activator nets -called safe nets with context arcs.The authors analyse in detail fundamental relationships between interval sequences and sequences of maximal antichains, and provide simple algorithms that transform one into another.

The conformance of a real time operating system (RTOS) to the OSEK/VDX standard is usually achieved by doing tests where a set of test cases is performed on the RTOS. However, in an embedded system, it is often necessary to specialize (configure) the code of the RTOS according to the requirements of the application. For such specialized RTOS, some conformance test cases can not be applied because they need some functionalities that are not supported anymore. This paper presents a model-based conformance verification of a RTOS with the OSEK/VDX standard. The method is applied on Trampoline RTOS which is used both for industry and academic purposes and which have been entirely and formally modeled by a product of extended finite automata embedding its source code. The first step is the construction of a complete model that describes the interaction between the application and the RTOS. In the second step all OSEK/VDX conformance test cases are translated into observers and composed with the complete model. Then, for a particular application, The observers allow to check if the RTOS model meets the OSEK/VDX specification. The interest of our approach is twofold: i) it allows to check the OSEK/VDX conformance of the complete version of the Trampoline RTOS; ii) for a specialized version of the RTOS, it identifies the relevant test cases for the given application, that require a very carefully conformance testing.

Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.

An Automated Driving System (ADS) is subject to hazardous weather conditions and to failures, both of which can result in a partial or total loss of its ability to monitor the driving environment. Yet until high driving automation and full driving automation is achieved, a human driver is expected to respond appropriately to any malfunction or adverse on-road conditions preventing the ADS from reliably sustaining the dynamic driving task performance. However, automation causes drowsiness and hypo-vigilance, which can compromise a human driver's ability to respond to ADS-issued requests. Hence the necessity of defining dynamic driving task fallback strategies that can be performed by the ADS, if and when necessary. The proposed fallback strategy is aimed at level 4 ADS features designed to operate a vehicle on a road whose characteristics make any attempt at stopping hazardous. It naturally applies to level 5 ADS-operated vehicles and to ADS-dedicated vehicles as well. The transition stage, during which the strategy is triggered, consists in the replacement of missing vehicles and obstacles in the world model with ghost objects. An embedded visibility map is then used to retrieve the maximum distance at which the ADS-operated vehicle can be seen, when driving behind it. The speed profile underlying the fallback strategy meets a time to collision criterion of 4 s, which enables the avoidance and the mitigation of rear-end collisions. The behaviour of drivers in collision imminent situations cannot be observed in test track studies due to safety concerns. As a result, experiments were conducted in the driving simulation software SCANeR studio.

In an embedded system, the specialization of the code of the real-time operating system (RTOS) according to the requirements of the application allows one to remove unused services and other sources of dead code from the binary program. The typical specialization process is based on a mix of precompiler macros and build scripts, both of which are known for being sources of errors. In this article, we present a new model-based approach to the design of application-specific RTOS. Starting with finite state models describing the RTOS and the application requirements, the set of blocks in the RTOS code actually used by the application is automatically computed. This set is used to build an application-specific RTOS model. This model is fed into a code generator to produce the source code of an application-specific RTOS. It is also used to carry on model-based validations and verifications, including the formal verification that the specialization process did not introduce unwanted behaviors or suppress expected ones. To demonstrate the feasibility of this approach, it is applied to specialize Trampoline, an open-source implementation of the AUTOSAR OS standard, to an industrial case study from the automotive domain.

We introduce a new model for the design of concurrent stochastic real-time systems. Probabilistic time Petri nets (PTPN) are an extension of time Petri nets in which the output of tokens is randomised. Such a design allows us to elegantly solve the hard problem of combining probabilities and concurrency. This model further benefits from the concision and expressive power of Petri nets. Furthermore, the usual tools for the analysis of time Petri nets can easily be adapted to our probabilistic setting. More precisely, we show how a Markov decision process (MDP) can be derived from the classic atomic state class graph construction. We then establish that the schedulers of the PTPN and the adversaries of the MDP induce the same Markov chains. As a result, this construction notably preserves the lower and upper bounds on the probability of reaching a given target marking. We also prove that the simpler original state class graph construction cannot be adapted in a similar manner for this purpose.

We provide a subclass of parametric timed automata (PTA) that we can actually and efficiently analyze, and we argue that it retains most of the practical usefulness of PTA for the modeling of real-time systems. The currently most useful known subclass of PTA, L/U automata, has a strong syntactical restriction for practical purposes, and we show that the associated theoretical results are mixed. We therefore advocate for a different restriction scheme: since in classical timed automata, real-valued clocks are always compared to integers for all practical purposes, we also search for parameter values as bounded integers. We show that the problem of the existence of parameter values such that some TCTL property is satisfied is PSPACE-complete. In such a setting, we can of course synthesize all the values of parameters and we give symbolic algorithms, for reachability and unavoidability properties, to do it efficiently, i.e., without an explicit enumeration. This also has the practical advantage of giving the result as symbolic constraints between the parameters. We finally report on a few experimental results to illustrate the practical usefulness of our approach.

Networks of Timed Automata (NTA) and Time Petri Nets (TPNs) are well-established formalisms used to model, analyze and control industrial real-time systems. The underlying theories are usually developed in different scientific communities and both formalisms have distinct strong points: for instance, conciseness for TPNs and a more flexible notion of urgency for NTA. The objective of the paper is to introduce a new model allowing the joint use of both TPNs and NTA for the modeling of timed systems. We call it Clock Transition System (CTS). This new model incorporates the advantages of the structure of Petri nets, while introducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency is introduced by a separate description of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we identify subclasses of CTSs equivalent by isomorphism of their operational semantics and provide (syntactic) translations. The classical state-space computation developed for NTA and then adapted to TPNs can easily be defined for general CTSs. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate theoretical and practical model to factor out the upcoming developments in the TPNs and the NTA scientific communities.

Currently the development of embedded software managing hardware devices that fulfills industrial constraints (safety, real time constraints) is a very complex task. To allow an increased reusability between projects, generic device drivers have been developed in order to be used in a wide range of applications. Usually the level of gener-icity of such drivers require a lot of configuration code, which is often generated. However, a generic driver requires a lot of configuration and need more computing power and more memory needs than a specific driver. This paper presents a more efficient methodology to solve this issue based on a formal modeling of the device and the application. Starting from this modeling, we use well-known game theory techniques to solve the driver model synthesis problem. The resulting model is then translated into the actual driver embedded code with respect to an implementation model. By isolating the model of the device, we allow more reusability and interoperability between devices for a given application, while generating an application-specific driver.

With this contribution, we aim to draw a comprehensive classification of Petri nets with stopwatches w.r.t. expressiveness and decidability issues. This topic is too ambitious to be summarized in a single paper. That is why we present our results in two different parts. The scope of this first paper is to address the general results that apply for both dense-time and discrete-time semantics. We study the class of bounded Petri nets with stopwatches and reset arcs (rSwPNs), which is an extension of T-time Petri nets (TPNs) where time is associated with transitions. Stopwatches can be reset, stopped and started. We give the formal dense-time and discrete-time semantics of these models in terms of Transition Systems. We study the expressiveness of rSwPNs and its subclasses w.r.t. (weak) bisimilarity (behavioral semantics). The main results are following: 1) bounded rSw- PNs and 1-safe rSwPNs are equally expressive; 2) For all models, reset arcs add expressiveness. 3) The resulting partial classification of models is given by a set of relations explained in Fig. 7: in the forthcoming paper, we will complete these results by covering expressiveness and decidability issues when discrete-time nets are considered. For the sake of simplicity, our results are explained on a model such that the stopwatches behaviors are expressed using inhibitor arcs. Our conclusions can however be easily extended to the general class of Stopwatch Petri nets.

With this contribution, we aim to draw a comprehensive classification of Petri nets with stopwatches w.r.t. expressiveness and decidability issues. This topic is too ambitious to be summarized in a single paper. That is why we present our results in two different parts. In the first part of our work, we established new results regarding to both dense-time and discrete-time semantics. We now focus on the discrete-time specificities. We address the class of bounded Petri nets with stopwatches and reset arcs (rSwPNs), which is an extension of T-time Petri nets (TPNs) where time is associated with transitions. Stopwatches can be reset, stopped and started. We recall the formal dense-time and discrete-time semantics of these models in terms of Transition Systems. We study the expressiveness of rSwPNs and its subclasses w.r.t. (weak) bisimilarity (behavioral semantics). The main results are following: 1) Discrete-time bounded TPNs, discrete-time bounded rSwPNs and untimed Petri nets are equally expressive; 2) The resulting (final) classification of models is given by a set of relations explained in Fig. 7. While investigating expressiveness, we exhibit proofs that can be easily extended to the resolution of decidability issues. Among other results, we prove that, for bounded rSwPNs, the state and marking reachability problems - undecidable with dense-time semantics - are decidable when discrete-time is considered. Table 1 gives a synthesis of the main decidability results for these models. For the sake of simplicity, our results are explained on a model such that the stopwatches behaviors are expressed using inhibitor arcs. Our conclusions can however be easily extended to the general class of Stopwatch Petri nets.

We consider Time Petri Nets (TPN) for which a firing time interval is associated with each transition. State space abstractions for TPN preserving various classes of properties (LTL, CTL and CTL∗) can be computed, in terms of so called state classes. Some methods were proposed to check quantitative timed properties but are not suitable for effective verification of properties of real-life systems. In this article, we consider subscript TCTL for TPN (TPN-TCTL) for which temporal operators are extended with a time interval, specifying a time constraint on the firing sequences. We prove the decidability of TPN-TCTL on bounded TPN and give its theoretical complexity. We propose a zone-based state space abstraction that preserves marking reachability and traces of the TPN. As for Timed Automata (TA), the abstraction may use an over-approximation operator on zones to enforce the termination. A coarser (and efficient) abstraction is then provided and proved exact w.r.t. marking reachability and traces (LTL properties). Finally, we consider a subset of TPN-TCTL properties (TPN-TCTLS) for which it is possible to propose efficient on-the-fly model-checking algorithms. Our approach consists in computing and exploring the zone-based state space abstraction. On a practical point of view, the method is integrated in Romeo [Gardey et al. (2005, Proceedings of 17th International Conference on CAV’05, Vol. 3576 of Lecture Notes in Computer Science, 418–423)], a tool for TPN edition and analysis. In addition to the old features it is now possible to effectively verify a subset of TCTL directly on TPN.

This paper describes a contribution to the verification of AADL models. It focuses on the part of the language dealing with operating modes. An analysis of the AADL mode change protocol is provided. Then, a translation process is exposed, that takes as an input an AADL model and produces as an output a Time Petri Net. Lastly, it is explained how the resulting Time Petri Net model can be used to (formally) verify some real-time properties of the AADL model.

Safety analysis in systems engineering (SE) processes, as usually implemented, rarely relies on formal methods such as model checking since such techniques, however powerful and mature, are deemed too complex for efficient use. This paper thus aims at improving the verification practice in SE design: considering the widely-used model of enhanced function flow block diagrams (EFFBDs), it formally establishes its syntax and behavioral semantics. It also proposes a structural translation of EFFBDs to transition time Petri nets ( TPNs); this translation is then proved to preserve the behavioral semantics (i.e., timed bisimilarity). After proving results on the boundedness of the resulting TPNs, it was possible to extend a number of fundamental properties (such as the decidability of liveness, state-access, etc.) from bounded TPNs to so-calledbounded EFFBDs. Finally, these results led to both implementing and integrating a formal verification tool within a development platform for system design for defense applications and in which the underlying complexity is totally concealed from the end-user.

The theory of Petri Nets provides a general framework to specify the behaviors of real-time reactive systems and Time Petri Nets were introduced to take also temporal specifications into account. We present in this paper a forward zone-based algorithm to compute the state space of a bounded Time Petri Net: the method is different and more efficient than the classical State Class Graph. We prove the algorithm to be exact with respect to the reachability problem. Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved to be timed bisimilar to the original Time Petri Net. As the method produce a single Timed Automaton, syntactical clocks reduction methods (DAWS and YOVINE for instance) may be applied to produce an automaton with fewer clocks. Then, our method allows to model-check T-TPN by the use of efficient Timed Automata tools.

In this paper, we present a method for the timed analysis of real-time systems, taking into account the scheduling constraints. The model considered is an extension of time Petri nets, scheduling extended time Petri nets (SETPN) for which the valuations of transitions may be stopped and resumed, thus allowing the modelling of preemption. This model has a great expressivity and allows a very natural modelling. The method we propose consists of precomputing, with a fast algorithm, the state space of the SETPN as a stopwatch automaton (SWA). This stopwatch automaton is proven timed bisimilar to the SETPN, so we can perform the timed analysis of the SETPN through it with the tool on linear hybrid automata, HYTECH. The main interests of this precomputation are that it is fast because it is difference bounds matrix (DBM)-based, and that it has online stopwatch reduction mechanisms. Consequently, the resulting stopwatch automaton has, in the general case, a fairly lower number of stopwatches than what could be obtained by a direct modelling of the system as SWA. Since the number of stopwatches is critical for the complexity of the verification, the method increases the efficiency of the timed analysis of the system, and in some cases may just make it possible at all.

In order to establish the temporal properties of real-time systems, we consider the timed Petri net (TPN) model. First, we prove that properties like the minimal (or maximal) firing time and the minimal (or maximal) time interval between the firing of two transitions can be established with a discrete analysis of a TPN. Then we propose to express the entire discrete execution sequence of the TPN by an automaton which considers the discrete passing of time as the occurrence of a dedicated event. The advantage is that this automaton can be efficiently analysed by using binary decision diagrams (BDDs). We have implemented every step of this approach.