International audience

International audience

Formal verification of SysML models contributes to detect design errors early in the life cycle of systems. Incremental modeling of systems leads to repeat verification of systems models parts that were already verified in previous versions of the SysML model. This paper proposes to optimize the verification process by generating first a dependency graph of the SysML model. The dependency generation algorithm is implemented by free SysML tool TTool. An Avionics Full DupleX network serves as case study.

Use case driven analysis is the corner stone of software and systems modeling in UML and SysML, respectively. Whether many books and tutorials have discussed the use of use case diagrams, students and industry practitioners regularly face methodological problems in writing good use cases. This paper defines a methodological assistant that helps designing use case diagrams relying on formalized rules and reuse of previous diagrams. The methodological assistant is implemented in Python. It is interfaced with the free SysML software TTool, and with Cameo Systems Modeler.

Finding the set of optimal architectures is an important challenge for the designer who uses the Model-Based System Engineering with SysML. The paper discusses the application of techniques to solve a Constraint Satisfaction Multi-criteria Optimization Problem (CSMOP) obtained from a SysML model. In this paper, we present our methodology and propose several stereotypes for model variability, including continuous and discrete variables. Then we define a new parametric diagram usage for context modeling optimization. From this optimization context and model variability, it is possible to generate a problem description file for the PyOpt optimization framework. Finally a case study combining optical and electronic parameters illustrates the methodology with numerical results.

International audience

Time Petri nets with stopwatches not only model system/environment interactions and time constraints. They further enable modeling of suspend/resume operations in real-time systems. Assuming the modelled systems are non deterministic and partially observable, the paper proposes a test generation approach which implements an online testing policy and outputs test results that are valid for the (part of the) selected environment. A relativized conformance relation named rswtioco is defined and a test generation algorithm is presented. The proposed approach is illustrated on an example.

The formal description technique RT-LOTOS has been selected as intermediate language to add formality to a real-time UML profile named TURTLE. For this sake, an RT-LOTOS verification platform has been developed for early detection of design errors in real-time system models. The paper discusses an extension of the platform by inclusion of verification tools developed for time Petri nets. The starting point is the definition of RT-LOTOS to TPN translation patterns. In particular, we introduce the concept of components embedding time Petri nets. The translation patterns are implemented in a prototype tool which takes as input an RT-LOTOS specification and outputs a TPN in the format admitted by the TINA tool. The efficiency of the proposed solution has been demonstrated on various case studies.

We present a UML 1.5 profile named TURTLE (Timed UML and RT-LOTOS Environment) endowed with a formal semantics given in terms of RT-LOTOS. TURTLE relies on UML's extensibility mechanisms to enhance class and activity diagrams. Class diagrams are extended with specialized classes named Tclasses, which communicate and synchronize through gates. Also, associations between Tclasses are attributed by a composition operator (Parallel, Synchro, Invocation, Sequence, or Preemption) which provides them with a formal semantics. TURTLE extends UML activity diagrams with synchronization actions and temporal operators (deterministic delay, nondeterministic delay, time-limited offer, and time-capture). The real-time dimension of TURTLE has been further improved by the addition of two composition operators, periodic and suspend, as well as suspendable delay, latency, and time-limited offer operators at the activity diagram level. Core characteristics of TURLE are supported by TTool - the TURTLE toolkit - which includes a diagram editor, a RT-LOTOS code generator and a result analyzer. The toolkit reuses RTL, a RT-LOTOS validation tool offering debug-oriented simulation and exhaustive analysis. TTool hides RT-LOTOS to the end-user and allows him/her to directly check TURTLE modeling against logical errors and timing inconsistencies. Besides the foundations of the TURTLE profile, this paper also discusses its application in the context of space-based embedded software.

The paper introduces a unified formal model for the complete and accurate specification of both temporal and logical (i.e., link) synchronization within hypermedia distributed and weakly synchronous systems. This new model extends time Petri nets with hierarchical design capabilities and new firing rules. These new firing rules enlighten the notion of hypermedia synchronization through powerful combinations of temporal and logical synchronization. Moreover, the proposed model offers an easy and concise modeling technique of asynchronous events in hypermedia systems.