16 Result(s)
within
Pierre de Saqui-Sannes
-
Chapter and Conference Paper
Dependency Graphs to Boost the Verification of SysML Models
Model-Based Systems Engineering has often been associated with the Systems Modeling Language. Several SysML tools offer formal verification capabilities, and therefore enable early detection of design errors i...
-
Chapter and Conference Paper
A Methodological Assistant for UML and SysML Use Case Diagrams
Use case driven analysis is the corner stone of software and systems modeling in UML and SysML, respectively. A use case diagram identifies the main functions to be offered by the system and showcases the inte...
-
Article
Trade-off analysis for SysML models using decision points and CSPs
The expected benefits of model-based systems engineering (MBSE) include assistance to the system designer in finding the set of optimal architectures and making trade-off analysis. Design objectives such as co...
-
Chapter and Conference Paper
Architecture Optimization with SysML Modeling: A Case Study Using Variability
Obtaining the set of trade-off architectures from a SysML model is an important objective for the system designer. To achieve this goal, we propose a methodology combining SysML with the variability concept an...
-
Chapter and Conference Paper
Static Analysis Techniques to Verify Mutual Exclusion Situations within SysML Models
AVATAR is a real-time extension of SysML supported by the TTool open-source toolkit. So far, formal verification of AVATAR models has relied on reachability techniques that face a state explosion problem. The ...
-
Chapter and Conference Paper
Testing Real-Time Systems Using TINA
The paper presents a technique for model-based black-box conformance testing of real-time systems using the Time Petri Net Analyzer TINA. Such test suites are derived from a prioritized time Petri net composed...
-
Article
TURTLE-P: a UML profile for the formal validation of critical and distributed systems
The timed UML and RT-LOTOS environment, or TURTLE for short, extends UML class and activity diagrams with composition and temporal operators. TURTLE is a real-time UML profile with a formal semantics expressed...
-
Article
Un environnement de conception de systèmes distribués basé sur UML
Cet article propose un nouvel environnement de développement des systèmes distribués, basé sur le profilUml turtle. Aux étapes d’analyse et de conception qui firent l’objet de précédents articles, nous ajoutons u...
-
Chapter and Conference Paper
Map** RT-LOTOS Specifications into Time Petri Nets
RT-LOTOS is a timed process algebra which enables compact and abstract specification of real-time systems. This paper proposes and illustrates a structural translation of RT-LOTOS terms into behaviorally equiv...
-
Chapter and Conference Paper
Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets
The paper describes a transformational approach for the specification and formal verification of concurrent and real-time systems.At upper level, one system is specified using the timed process algebra RT-LOTO...
-
Chapter and Conference Paper
New Operators for the TURTLE Real-Time UML Profile
In a previous paper, we defined TURTLE, a Timed UML and RT-LOTOS Environment which includes a real-time UML profile with a formal semantics given in terms of translation to RT-LOTOS, and a model validation app...
-
Article
Multimedia Authoring with Hierarchical Timed Stream Petri Nets and Java
The expected benefits of modeling documents using a formal technique are twofold. First, the document's model can be checked against logical errors and unsatisfied timing constraints. Second, the same model ca...
-
Chapter
Verification by abstraction as a preamble for interoperability test suite generation
In [2], we proposed a verification by abstraction approach for protocol specifications written in Estelle*, an enhanced Estelle with a rendezvous mechanism. The protocol’s reachability graph is labeled with occur...
-
Chapter and Conference Paper
Hierarchical Time Stream Petri Net: A model for hypermedia systems
The paper proposes a new class of timed Petri nets for the specification of temporal constraints and description of logical behaviour in distributed hypermedia systems. In particular, hierarchical design capab...
-
Article
Toward a formal specification of multimedia synchronization scenarios
This paper introduces time stream Pétri nets (Ts treamPn), a model for the formal specification of multimedia synchronization scenarios. This new model extends time Pétri nets to formally describe the timed behav...
-
Chapter and Conference Paper
Basic synchronisation concepts in multimedia systems
Multimedia systems were so far primarily addressed with communication and performance in mind. It is now acknowledged they essentially capture synchronisation problems, at communication and application levels,...
