Retour au site du LAAS-CNRS

Mots-Clés / Keywords

Abstract

In a companion paper [BPV06], we investigated the expressiveness of Time Petri Nets extended with Priorities and showed that it is very close to that Timed Automata, in terms of weak timed bisimilarity. As a continuation of this work we investigate here the applicability of the available state space abstractions for Bounded Time Petri Nets to Bounded Prioritized Time Petri Nets. We show in particular that a slight extension of the strong state classes construction of [BV03] provides a convenient state space abstraction for these nets, preserving markings, states, and LTL formulas. Interestingly, and conversely to Timed Automata, the construction proposed does not require to compute polyhedra differences.

Abstract

The development process of complex systems needs to take in account differents domains and aspects. SysML (Systems Modeling Language) is a new modeling lan guage that allows a system description with various inte grated diagrams (as structure, behavior and requirements diagrams), but SysML lacks formality for the requirement verification. The aim of this paper is to propose an ap proach to verify complex systems using SysML as a lan guage which describes the system structure and require ments. Petri nets and temporal logic LTL are used respec tively to formalize the system behavior and requirements. The benefit of such formalization is to allow an automatic formal verification. In order to demonstrate this method ology, it will be used a factory automation system, mod eled by SysML and Petri nets, and verified by the TINA toolbox.

Abstract

Several extensions of Time Petri nets (TPNs) have been proposed for modeling suspension and resumption of actions in timed systems. We first introduce a simple class of TPNs extended with stopwatches (SwTPNs), and present a semi-algorithm for building exact representations of the behavior of SwTPNs, based on the known state class method for Time Petri nets. Then, we prove that state reachability in SwTPNs and all similar models is undecidable, even when bounded, which solves an open problem. Finally, we discuss overapproximation methods yielding finite abstractions of their behavior for a subclass of bounded SwTPNs, and propose a new one based on a quantization of the polyhedra representing temporal information. By adjusting a parameter, the exact behavior can be approximated as closely as desired. The methods have been implemented, experiments are reported.

Abstract

More and more, models, through Domain Specific Languages (DSL), tend to be the solution to define complex systems. Expressing properties specific to these metamodels and checking them appear as an urgent need. Until now, the only complete industrial solutions that are available consider structural properties such as the ones that could be expressed in OCL. There are although some attempts on behavioural properties for DSL. This paper addresses a method to specify and then check temporal properties over models. The case study is SimplePDL, a process metamodel. We propose a way to use a temporal extension of OCL, TOCL, to express properties. We specify a models transformation to Petri Nets and LTL formulae for both the process model and its associated temporal properties. We check these properties using a model checker and enrich the model with the analysis results. This work is a first step towards a generic framework to specify and effectively check temporal properties over arbitrary models.

Mots-Clés / Keywords

Mots-Clés / Keywords