|
Written by Agusti Canals
|
NEPTUNE'2010 s'est conclu hier à 18h30 par une table ronde sur SysML ...

NEPTUNE'2010 s'est conclu hier à 18h30 par une table ronde sur SysML qui a regroupé une 30aine de personnes !!, les deux journées ont été un succès, en moyenne 65 présents. Les transparents sont déjà sur le site web, n'hésitez pas à les consulter et à poser vos questions aux intervenants par mail ... A noter que les synthèses des tables rondes arriveront bientôt. On peut déjà dire que les Méthodes formelles, mais aussi SysML se rapprochent fortement du MDE et que le rêve peut devenir réalité. Merci aux orateurs, animateurs, et participants aux tables ronde pour leur implication et leur motivation. Merci aussi à tous les participants qui j'espère ont apprécié les différents "talks", et rendez vous donc en 2011 à Paris !
Vu sur http://www.dotnetguru2.org/acanals/index.php |
NEPTUNE workshop 2010
May 18th, 2010
09h00-09h15 |
Welcome and overview
|
A. Canals (CS) |
|
| 09h15-10h00 |
Model inside
|
T. Lecomte (Clearsy) |
|
| 10h00-10h30 |
MDE: Current issues |
F. Kordon (LIP6, Univ. P. & M. Curie) |
|
| 11h00-11h30 |
Petri nets standardization: state of the art and future challenges
|
L. Hillah (LIP6 et Univ. Paris Ouest Nanterre La Défense) et L. Petrucci (LIPN, Univ. Paris 13)) |
|
| 11h30-12h00 |
Definition of a family pattern transformation models for the analysis of AADL models |
X. Renault (LIP6, Univ. P. & M. Curie) et J. Hugues (ISAE)
|
|
| 14h00-14h30 |
OMEGA2 - Profile & tools for system modelling and verification with UML 2.x & SysML |
Iulian Ober, I. Dragomir (IRIT/MACAO) |
|
|
Formal Methods Integration in the software development process
|
I. Perseil (INSERM) et P. Leblanc (IBM) |
|
| 14h30-15h00 |
Design of a data-processing safety module with a generic functional software, interpretable and validable formaly |
M. Antoni (SNCF) |
|
| 15h30-16h00 |
Synopsis and perspectives of the SPaCIFY project : Model-Driven Engineering and Formal Methods for Spacecraft Systems
|
A. Cortier (CNES-IRIT/ACADIE), P. Arberet (CNES), G. Garcia (Thales Alenia Space), A.-E. Rugina (Astrium) |
|
| 16h00-16h30 |
TACOS - Trustworthy Assembling of Components: frOm requirements to Specifications |
H. Mountassir (Univ. de Franche-Comté) |
|
| 16h30-17h30 |
Wrap-up and Round Table
MDE and Formal Methods : close future?
|
I. Ober (IRIT/MACAO), F. Kordon (LIP6, Univ. P. & M. Curie), I. Perseil (INSERM), A. Rossignol (ASTRIUM)
|
|
May 19th, 2010
| 09h15-09h30 |
Welcome and overview
|
T. Millan (IRIT) |
|
| 09h30-10h35 |
Keynote: MDE: from design-time to runtime |
J.-M. Jezequel (Univ. Rennes 1 & INRIA) |
|
| 10h35-11h10 |
Applying MDE for the validation of correct Eclipse Plugin Bundles |
G. Doux, M. Didonet del Fabro, F. Jouault, P. Albert, J. Bezivin, F. Madiot, S. Lee |
|
| 11h45-12h20 |
Flexibility in embedded real-time applications: the Flex-eware Project
|
J. Pulou (Orange-telecom) |
|
| 12h20-12h55 |
Applying MDE to Embedded System Design: First results and perspectives from the Lambda project |
S. Demathieu (Thales), Y. Bernard (Airbus), L. Maillet-Contoz, (ST Microelectronics), M. Bordin, (Adacore) et F. Mallet (INRIA) |
|
| 14h30-15h05 |
Assessing quality in SysML models
|
O. Casse et M. Hause (Artisan) |
|
| 15h05-15h40 |
VETESS : MDE, Testing approaches and SysML |
F. Fondement (Univ. de Haute Alsace), F. Peureux (Univ. de Franche-Comté), B. Legeard (Smartesting), C. Scherrer, M. Alter (Clemessy) |
|
| 16h15-16h50 |
Functional validation with a practical SysML / Simulink transformation
|
R. Snyder, D. Bocktaels, X. Feigenbaum (B2i automotive Engineering, Rungis, France) |
|
| 16h50-17h25 |
A SysML Based Approach to Perform FMEA |
J. Shi, O. Alt, W. Kling, F. Schreiner |
|
| 17h25-18h25 |
Wrap-up and Round Table
MDE and SysML, MDE and embedded systems: close future?
|
J.-M. Bruel (IRIT/MACAO), P. Roques (A2-ARTAL), F. Fondement (Univ. de Haute Alsace), X. Feigenbaum (B2i automotive Engineering, Rungis, France), J.-M. Jezequel (Univ. Rennes 1 & INRIA)
|
 |
Papers will be published in "Génie Logiciel - Magazine de l'ingéniérie du logiciel et des systèmes" during June 2010 Génie Logiciel - Magazine de l'ingéniérie du logiciel et des systèmes - GL & IS - 8, rue du Parc - 92190 MEUDON
|
|
Written by Administrator
|
Thierry Lecomte
Modelling is an ever-growing engineering activity. When searching for a sound way of managing the complexity of the systems he is working with, an Engineer might be tempted to go for formal methods in order to provide a more rigorous framework to his development. Mathematization is the price to pay for obtaining a higher level of confidence, as well as emerging difficulties that were probably not expected initially. This article presents several use cases, from several domains, where pros and cons for using formal methods are exposed.
La modélisation est une activité qui tend à prendre de l’ampleur dans le monde de l’Ingénieur. Dans sa recherche d’une solution adaptée à la complexité des systèmes qu’il manipule, l’Ingénieur peut être amené à avoir recours aux méthodes formelles afin d’offrir un cadre plus rigoureux à ses travaux. Le prix à payer pour obtenir un niveau de confiance plus élevé est une mathématisation du développement et l’apparition de difficultés qui n’avaient peut-être pas été initialement prévues. Cet article présente plusieurs cas d’utilisation, dans des domaines variés, où sont exposés les bienfaits mais aussi les difficultés induits par le recours à la modélisation formelle. |
|
Model Driven Engineering : Some Current Issues |
|
|
|
Fabrice Kordon
LIP6, CNRS UMR 7606, Université P. & M. Curie, 4 place Jussieu, 75252 Paris Cedex 05
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
Model Driven Engineering (MDE) is more and more popular in industrial development. Its objective is to focus on models that serve as a basis for development. This leads to the elaboration of software development processes that are tooled and that help engineers to tackle the problem of system reliability.
So far, MDE elaborated techniques to: 1) elaborate languages or semi-formal notations by means of meta-models; 2) define mapping rules between meta-models; 3) express consistency constraints to be checked on models; 4) define engineering processes. These techniques are now mature and various implementations are now widely accepted and used (for instance, in the Eclipse framework). However, new issues are rising; two of them are discussed here.
The first issues deals with the management of formal semantics. This is a need for several classes of critical applications where MDE approaches can be used. However, the mathematic-based semantics of formal notations is difficult to capture by means of meta-models. Some work has been done these past years in the context of the ISO/IEC Petri Net standard. It is of interest because Petri nets are in fact a set of related (but different) formal notations, making the context even more difficult.
The second one deals with the use of formal methods in a methodological context. This is even more difficult when the reasoning provided by formal methods takes place all over the software design and development process. To achieve this, engineers need a pivot language that serves as a basis for modeling as well as translation to adequate formal description techniques for verification purpose. An interesting experience has been proposed with AADL in the context of embedded systems, that are often critical by nature.
Ingénierie basée sur les modèles : quelques défis actuels
L’Ingénierie basée sur les modèles (ou MDE pour Model Driven Engineering) est une approche de plus en plus présente dans le monde industriel. L’objectif est de centrer le développement de systèmes sur des modèles qui accompagnent leur conception et servent de base à leur développement. On est donc dans une phase de mise en place systématique de processus de fabrication logicielle instrumentés en vue de mieux maîtriser la fiabilité des systèmes ainsi produits.
Jusqu’à présent, le MDE a établi des techniques permettant : 1) de définir des langages ou notations semi-formelles au moyen de méta-modèles ; 2) d’exprimer des règles de transformations entre méta-modèles ; 3) d’exprimer des contraintes de cohérence sur des modèles ; 4) d’exprimer des procédés de fabrication. Ces techniques atteignent une maturité à travers des implémentations reconnues, par exemple au sein de l’environnement Eclipse. Cependant, de nouveaux défis sont en train d’apparaître et deux d’entre eux seront discutés ici.
Le premier concerne la gestion d’une sémantique formelle. Pour certaines classes d’applications critiques, de telles techniques doivent être mises en œuvre dans le cadre du MDE. Cependant, les modèles formels ont des sémantiques basées sur des notions mathématiques qu’il est difficile de capturer sous la forme de méta-modèles. Des travaux dans ce sens ont été effectués dans le cadre du standard ISO/IEC pour les réseaux de Petri et proposent une approche intéressante dans le cadre d’une sémantique rendue délicate par l’existence de différentes variations de cette notation formelle.
Le second concerne la mise en œuvre de méthodes formelles dans un contexte méthodologique. Ce point est particulièrement délicat lorsqu’il faut raisonner sur les modèles tout au long du processus de conception et fabrication logicielle. Pour y arriver, il faut à la fois disposer d’un langage pivot adéquat servant de base à la modélisation et pouvant être projeté sur différentes notations formelles à des fins d’analyse. Une expérience intéressante dans ce cadre a été menée avec AADL dans le domaine des systèmes embarqués, souvent critiques de par leur nature.
|
|
Petri nets standardisation: state of the art and future challenges |
|
|
|
|
Lom M. Hillah1 and Laure Petrucci2
1 LIP6, CNRS UMR 7606 et Université Paris Ouest Nanterre La Défense
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
2 LIPN, CNRS UMR 7030, Université Paris XIII
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
The Petri Nets community, including academic as well as industrial actors, noticed very early the lack of homogeneity both in formal definitions and tools. Indeed, there exists a complete panel of Petri net types, exhibiting sometimes significant differences (e.g. time Petri nets) or simple extensions only (such as nets with inhibitor arcs) Moreover, each tool uses its own Petri net kind and implements its specific analysis techniques.
Verifying systems modelled with Petri nets requires the combined use of multiple verification techniques, and thus of the numerous associated software tools. For practical feasibility, designing a Petri nets interchange format is a major issue.
The ISO/IEC-15909 standard aims at providing a response to this concern. It is structured into 3 parts.
The first part is concerned with definitions of the formalism, thus providing several usual Petri net types with a formal semantics: place/transition nets and high-level (coloured) nets. This part was published as an International Standard in December 2004. An amendment defining symmetric nets should be published soon.
The second part, published in November 2009, focuses on syntax and design of a Petri nets interchange format. This language, namely PNML (Petri Net Markup Language), is grounded on the concepts defined by the first part of the standard. Its design is based on UML metamodels, and then a transformation to XML. This approach purposefully takes on a high level design, independently of any concrete representation technology. A semantic mapping with part 1’s formal definitions is thus established through the metamodels-based definitions. This approach adopted in the development of the second part of the standard was experimented for place/transition and symmetric nets, through a set of programming interfaces (API) generated from the metamodels. The library thus obtained provides all the import and export functions between a Petri net model and PNML, necessary for a tool developer to handle PNML, without requiring a deep knowledge of the standard.
One of the major issues in part 2 was flexibility and extensibility of the PNML language, planning for the work on part 3 of the standard. This development on part 3 just started. It is concerned with Petri net extensions. This area being rather large, a first task consisted in delimiting the research area, as well as setting priorities. The outcomes are the choice of model structuring issues (modular, hierarchical Petri nets, etc.) and mechanisms necessary for integrating new Petri net kinds and new elements (such as inhibitor arcs).
Standardisation des réseaux de Petri : état de l’art et enjeux futurs
La communauté travaillant sur les réseaux de Petri, aussi bien universitaires qu'industriels, a constaté relativement tôt le manque d'homogénéité dans les définitions formelles et les outils. En effet, toute une panoplie de types de réseaux de Petri existe, avec des différences parfois significatives (par exemple les réseaux temporels) ou de simples extensions (comme les réseaux avec arcs inhibiteurs). De plus, chaque outil utilise sa propre version de réseau de Petri et implémente des techniques d'analyse qui lui sont propres.
La vérification de systèmes modélisés avec des réseaux de Petri nécessite l'utilisation de diverses techniques de vérification, donc des divers outils associés. Pour que cette démarche soit réalisable dans la pratique, la conception d'un format d’échange de réseaux de Petri entre ces outils est un enjeu majeur.
Le standard ISO/IEC-15909 a pour objectif de répondre à cette problématique. Il est structuré en 3 parties.
La première partie concerne les définitions du formalisme, donnant ainsi une sémantique formelle à plusieurs types usuels de réseaux de Petri : les réseaux places/transitions et les réseaux de haut niveau (colorés). Cette partie a été publiée comme standard international en décembre 2004. Un amendement définissant les réseaux symétriques devrait être publié sous peu.
La seconde partie, parue en novembre 2009, se concentre sur la syntaxe et l'élaboration d'un langage d'échange de réseaux de Petri. Ce langage, PNML (Petri Net Markup Language) reprend les concepts introduits dans les définitions de la première partie du standard. Sa conception repose sur des métamodèles UML, puis une transformation en XML. Cette approche prend le parti d’une conception d’abord de haut niveau, indépendamment de toute technologie de représentation concrète. Ainsi, à travers la définition basée sur les métamodèles, une mise en correspondance sémantique avec les définitions formelles de la première partie est établie. Cette approche adoptée dans le développement de la seconde partie du standard a été expérimentée pour les réseaux places/transitions et symétriques au travers d'un ensemble d'interfaces de programmation (API) générés à partir des métamodèles. La bibliothèque ainsi produite fournit toutes les fonctions d'import et d'export de modèles de réseaux de Petri en PNML nécessaires à un développeur d'outil, sans requérir de sa part une connaissance approfondie du standard.
Un des enjeux majeurs de la seconde partie a été la flexibilité et l'extensibilité du langage PNML, en vue des travaux sur la troisième partie du standard. Le développement de cette troisième partie vient de démarrer. Elle porte sur les extensions de réseaux de Petri. Ce domaine étant particulièrement vaste, il a fallu dans un premier temps délimiter le cadre dans lequel ces recherches allaient s'inscrire, ainsi que des priorités. Les choix se sont portés d'une part sur la structuration des modèles (réseaux de Petri modulaires, hiérarchiques, etc.) et d'autre part sur les mécanismes nécessaires à l'intégration de nouveaux types de réseaux de Petri et l'ajout de nouveaux éléments (tels que les arcs inhibiteurs). |
|
Definition of a family pattern transformation models for the analysis of AADL models |
|
|
|
X. Renault
LIP6, CNRS UMR 7606, Université P. & M. Curie, 4 place Jussieu, 75252 Paris Cedex 05
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
J. Hugues
Université de Toulouse, ISAE 10 avenue Edouard Belin - BP 54032 31055 Toulouse CEDEX 4
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
AADL (Architecture Analysis and Design Language) is an architecture description language to achieve a variety of analysis formal or semi-formal, such as static analysis or model checking techniques. AADL provides a level of abstraction to express many constructions for the realization of embedded real time systems. Meanwhile, we note that properties to check on these systems usually do cover just a subset of model elements (components or non-functional properties).
In this article, we show how to take advantage of this information to define several transformation patterns from AADL to Petri nets adapted to the property to check. The qualitative properties of the system (such as deadlock detection and traceability of messages exchanged) can be analyzed using Colored Petri nets, using the CPN-AMI toolsuite. The quantitative properties (such as scheduling system or verification of size of communication buffers) can be processed using Temporal Petri nets, using Tina. We present the development of generic patterns that can be annotated in accordance with the type of property to check. We show how these patterns can limit the combinatorial explosion by restricting the model to the only relevant blocks.
Définition d’une famille de patrons de transformation pour l’analyse de modèles AADL
AADL (Architecture Analysis and Design Language) est un langage de description d'architecture permettant une multitude d'analyses formelles ou semi-formelles, en utilisant par exemple d’analyses statiques, ou encore des techniques de model checking. AADL fournit un niveau d'abstraction intéressant pour exprimer de nombreuses constructions utiles à la réalisation de systèmes embarqués temps réels. Parallèlement, nous remarquons que les propriétés à vérifier sur ces systèmes ne couvrent bien souvent qu'un sous-ensemble des éléments du modèle (composants ou propriétés non-fonctionnelles).
Nous montrons dans cet article comment tirer parti de ces informations pour définir plusieurs patrons de transformation d'AADL vers les réseaux de Petri adaptés à la propriété à vérifier. Les propriétés qualitatives du système (comme la détection d'interblocage ou la traçabilité des messages échangés) peuvent être analysées à l'aide des réseaux de Petri colorés, en utilisant l'environnement CPN-AMI. Les propriétés quantitatives (comme l'ordonnancement du système ou la vérification du dimensionnement des buffers de communication) peuvent être traitées à l'aide des réseaux de Petri temporels, en utilisant l'environnement Tina. Nous nous sommes intéressés à l'élaboration de patrons génériques pouvant être annotés en accord avec le type de propriété à traiter. Nous montrons comment ces patrons permettent de limiter l'explosion combinatoire en restreignant le modèle à analyser aux seuls blocs utiles. |
|
Formal methods integration in the software development process |
|
|
|
|
Isabelle Perseil
The software development process is the main tool of project management. It serves to plan optimally all activities related to the production of software. It is essentially a scheduling policy of these activities which allows to control and to follow them in time. A given development process may or may not be applied in a methodological context (method or methodology) and in principle, is independent of any modeling and programming language used throughout the process.
First, we describe the most-value resulting from the use of an integrated process in a methodological approach, and then standardized. Secondly, we describe the state-of-the-art of good practices in software process development techniques described in avionics standards which concern the real-time and embedded systems (DO178C). At the same time, we present a state-of-the-art of the RUP (the IBM Rational Unified Process) with its advantages (iterative process, UC driven, and focused on the architecture), as well as a state-of-the-art of the methodologies and the modeling languages that are used in the course of an avionics real-time and embedded development. This leads us to highlight the discrepancy between the evolution of modeling languages, the practices of model transformation and verification that ensure a level of a sufficient formalization and the evolution of the processes which use them during the phases of requirements specification, analysis, design and certified code generation. The immediate result is the emergence of a formal methods integration problematic allowing a better specifying, modeling and checking.
Very rare integration approaches have succeeded in industrial environments (Method B / Ada on the draft of the Meteor line, the platform Esterel studio for (Rational Rose) UML at Dassault, the model transformations of MARTE to more formal AADL models at Airbus as well as an intensive use of PVS for the verification of non-functional properties of complex systems at Nasa) but only on limited portions of the lifecycle. We moved here toward an adaptation of the RUP for real-time systems. First, our approach is to enrich the current process with other phases, then to consider that the requirements of strategic type must first be completely identified, specified, verified since they are those which lead all the development. We are redefining the lifecycle which puts the models of highest level of abstraction (analysis, architecture) as the main objectives to reach. The enrichment of the development process relates to additional phases and a parallelization of its sub-processes. The software development process that we propose is subdivided into three sub-processes whose principal is led by the strategic use cases. It is a seamless development involving intermediate languages to move gradually from the informal to the formal and which provides the opportunity to compose languages of different types.
Intégration des méthodes formelles dans le processus de développement
Le processus de développement logiciel est le principal outil du management de projet. Il sert à planifier de manière optimale l’ensemble des activités liées à la production de logiciel. Il comporte essentiellement une politique d’ordonnancement de ces activités qui permet de les piloter et de les suivre dans le temps. Un processus de développement donné peut ou non être appliqué dans un contexte méthodologique (méthode ou méthodologie) et en principe est indépendant des langages de modélisation et de programmation utilisés tout au long du processus.
Nous décrivons dans un premier temps la plus-value résultant de l’utilisation d’un processus intégré dans une démarche méthodologique, puis standardisé. Nous décrivons ensuite l’état de l’art des bonnes pratiques en matière de processus de développement décrites dans les normes avioniques qui concernent les systèmes temps-réel embarqués (DO178C). Parallèlement nous dressons un état de l’art du RUP avec ses avantages (processus itératif, UC driven, et centré sur l’architecture), ainsi qu’un état de l’art des méthodologies et langages de modélisation utilisés au cours d’un développement temps-réel embarqué de type avionique. Ceci nous amène à mettre en exergue la divergence entre l’évolution des langages de modélisation, les pratiques de vérification et de transformation de modèles qui garantissent un niveau de formalisation suffisant et l’évolution des processus qui les utilisent pendant les phases de spécification des exigences, analyse, conception, génération de code certifié. La conséquence directe est l’émergence d’une problématique d’intégration des méthodes formelles permettant de mieux spécifier, modéliser, vérifier.
De très rares approches d’intégration ont réussi en milieu industriel (Méthode B / Ada sur le projet de la ligne Meteor, la plateforme Esterel studio for (Rational Rose) UML chez Dassault, les transformations de modèles MARTE vers des modèles AADL plus formels chez Airbus ainsi qu’une utilisation intensive de PVS pour la vérification des propriétés non fonctionnelles de systèmes complexes à la Nasa) mais sur des portions limitées du cycle de vie. Nous nous sommes orientés ici vers une adaptation du RUP pour les systèmes temps réels. Notre approche consiste dans un premier temps à enrichir le processus actuel avec d’autres phases puis à considérer que les exigences de type stratégiques doivent d’abord être complètement identifiées, spécifiées, vérifiées puisque ce sont elles qui conduisent tout le développement. Nous redéfinissons le cycle de vie qui place les modèles de plus haut niveau d’abstraction (analyse, architecture) comme les principaux objectifs à atteindre. L’enrichissement du processus de développement porte sur des phases supplémentaires et une parallélisation de ses sous-processus. Le processus de développement que nous proposons se subdivise en trois sous-processus dont le principal est conduit par les cas stratégiques. Il s’agit d’un développement dit sans couture faisant intervenir des langages intermédiaires pour passer graduellement de l’informel au formel et qui fournit la possibilité de composer des langages de type différent. |
|
Design of a data-processing safety module with a generic functional software, interpretable and validable formally |
|
|
|
|
Written by Administrator
|
Marc Antoni
This article describes the principles having prevailed to the development of a automat with high level of safety and generic interpretable specifications which it carries out in real-time. The « functional software » consists of a whole of generic graphs « intanciated » according to the route plan of the station. The « functional software » obtained is validable formally. The safety of the computing systems cannot be estimated by probabilistic approaches, at least for an industrial use. Our experience shows that the major part of the risk of the safe systems does not come from random failures, but from systematic failures of the software due to definition errors. If there exists a case non covered by the specifications, each time the unconsidered configuration of the entries occurs, the functional will lead in a deterministic way to a unsure state of the system. It is a systematic defect which will end up being activated and producing, in a deterministic way, a dangerous situation. A tests generator would not assure that the exhaustiveness of the tests carried out. Their deposit rate is limited in particular with the difficulty of building tests to check the respect of functionalities, their were not considered at the time of the studies of the specifications. We defined an interpretable language of specification, the AEFD language (Deterministic Automat with Finite States). The idea consisted in developing an industrial safety automat which has a developmet tools which behave like an abstract machine (a competing event-driven automat with constraints at null time of transition) in order to allow a later formal validation of it. The writing of the functional graphs is addressed to people having a railway competence without any particular knowledge in data processing. The formal validation method of the safety properties (direct and indirect by the procedures and the operators) is resulting from an university work. It covers the whole cycle of the specification to the validation while passing by the execution and it rests on a mathematical proof. The approaches is like a “Model Checking” which would apply not on a “model” but on the executable target code (interpreted). We do not carry out tests scripts but we check completely that the system follows all the the safety properties and check that the awaited functional properties did not present superfluous conditions. The SNCF developed and deposited the tools and methods making it possible industrially to carry out these treatments during the realization of the tests before put into service.
Conception d’un module informatique critique avec fonctionnel applicatif générique, interprétable et validable formellement
Cet article se propose de décrire les principes ayant prévalus au développement d’un automate générique à haut niveau de sécurité et des spécifications interprétables qu’il exécute en temps réel. Le fonctionnel applicatif est constitué d’une ensemble de graphes génériques instanciés selon le plan de voie du poste. Le fonctionnel obtenu est validable formellement. La sécurité des systèmes informatiques ne peuvent être estimée par des approches probabilistes, du moins dès lors que le niveau visé est industriel. L’expérience montre que la majeure partie du risque des systèmes sûrs provient pas de défaillances aléatoires, mais de défaillances défaillances systématiques des logiciels dues à des erreurs de définition. S’il existe un cas non couvert par les spécifications, chaque fois que la configuration non envisagée des entrées va se produire, le fonctionnel va conduire de manière déterministe à un état non sûr du système, quelque soit son architecture matérielle et son niveau de sécurité au sens des normes actuelles. Il s’agit d’un défaut systématique qui finira par être activé et produire, de manière déterministe, une situation dangereuse. Les générateurs de tests ne donneraient aucune garantie quant à l’exhaustivité des tests effectués. Leur taux de couverture est limité notamment face à la difficulté de penser à bâtir des tests pour vérifier le respect de fonctionnalités non considérées lors des études de spécification. Pour ce faire, nous avons défini un langage de spécification interprétable, le langage AEFD (Automate à Etats Finis Déterministe). L’idée principale consistait à développer un automate industriel de sécurité qui dispose d’une chaîne de développement réutilisable à faible coût et qui se comporte comme une machine abstraite (un automate événementiel concurrentiel à contraintes à temps de transition nul) afin d’en permettre une validation formelle ultérieure. L’atelier d’écriture des graphes fonctionnels s’adresse à des personnes possédant une compétence métier sans aucune connaissance particulière en informatique. La méthode de validation formelle des propriétés de sécurité (direct et indirect par les procédures et les opérateurs) est issue des travaux universitaires. Elle couvre l’ensemble du cycle de la spécification à la validation en passant par l’exécution et elle repose sur une preuve mathématique. La démarche s’approche d’une démarche de "Model Checking" qui s’appliquerait non pas sur un «modèle» mais sur le code cible exécutable (interprété). Nous n’exécutons pas de scripts d’essais mais nous vérifions complètement que le système suit les propriétés de sécurité et les propriétés fonctionnelles attendues d’un moment à l’autre et ne présente pas de conditions superflues. La SNCF a développé et déposé les outils et méthodes permettant de réaliser industriellement ces traitements lors de la réalisation des essais avant mise en exploitation. |
|
Synopsis and perspectives of the SPaCIFY project: Model-Driven Engineering and Formal Methods for Spacecraft Systems |
|
|
|
Alexandre Cortier (CNES-IRIT/Acadie) Paul Arberet (CNES) Gerald Garcia (Thales Alenia Space) Ana-Elena Rugina (Astrium)
Flight software of spacecraft systems is mainly responsible for implementing command and control laws. The design of flight software has its own peculiarities and must meet severe requirements such as hard real time constraints, limited hardware resources capacity, remote observability and commandability and high level of quality and safety.
To improve productivity in the design stages of these systems, the SPaCIFY ANR exploratory project aims to define a development process and associated tools for hard time embedded space applications. The main originality of the approach is to combine Model Driven Engineering (MDE), formal methods and synchronous paradigms in a single homogeneous design process.
The ANR project SPaCIFY has designed and partially implemented a domain-specific environment, called Synoptic, for real-time embedded space application. Synoptic is an Eclipse-based modeling workbench which relies on open-source technologies. Synoptic supports many aspects of aerospace software design. As such, it is a domain-specific framework which provides the engineer with a unified modeling environment to handle heterogeneous analysis, design, implementation and verification tasks, as defined in collaboration with the industrial end users of the project. This article presents a synopsis of the proposed approach and gives an outlook of the perspectives of the project.
Les Logiciels de Vol implémentent les lois de commandes/contrôle des satellites. La conception de ces LV possède ses propres particularités et le logiciel produit doit satisfaire à des exigences fortes : contraintes temps-réel dures, capacité des ressources matérielles limitée, observabilité et commandabilité du système, haut degré de qualité et de sûreté.
Afin d’améliorer la productivité des étapes de conception de ces systèmes et d’améliorer la fiabilité des logiciels conçus, le projet exploratoire ANR SPaCIFY a défini et partiellement implémenté un environnement de conception dédié aux systèmes spatiaux embarqués et temps-réel. Cet environnement, appelé Synoptic, est constitué d’une suite d’outils basée sur des technologies Open-Source tel qu’Eclipse.
L’originalité de l’approche consiste à combiner l’Ingénierie Dirigée par les Modèles (IDM), les méthodes formelles et le paradigme synchrone dans un processus de développement homogène. Synoptic fournit un environnement de modélisation unifiée permettant à l’ingénieur d’effectuer les tâches de conception, de développement, d’implémentation, d’analyse et de vérification.des systèmes spatiaux. Cet article présente un synopsis de l’approche proposée et donne un aperçu des perspectives du projet SPaCIFY.
2 Abstract
This article describes the principles having prevailed to the development of a automat with high level of safety and generic interpretable specifications which it carries out in real-time. The « functional software » consists of a whole of generic graphs « intanciated » according to the route plan of the station. The « functional software » obtained is validable formally. The safety of the computing systems cannot be estimated by probabilistic approaches, at least for an industrial use. Our experience shows that the major part of the risk of the safe systems does not come from random failures, but from systematic failures of the software due to definition errors. If there exists a case non covered by the specifications, each time the unconsidered configuration of the entries occurs, the functional will lead in a deterministic way to a unsure state of the system. It is a systematic defect which will end up being activated and producing, in a deterministic way, a dangerous situation. A tests generator would not assure that the exhaustiveness of the tests carried out. Their deposit rate is limited in particular with the difficulty of building tests to check the respect of functionalities, their were not considered at the time of the studies of the specifications. We defined an interpretable language of specification, the AEFD language (Deterministic Automat with Finite States). The idea consisted in developing an industrial safety automat which has a developmet tools which behave like an abstract machine (a competing event-driven automat with constraints at null time of transition) in order to allow a later formal validation of it. The writing of the functional graphs is addressed to people having a railway competence without any particular knowledge in data processing. The formal validation method of the safety properties (direct and indirect by the procedures and the operators) is resulting from an university work. It covers the whole cycle of the specification to the validation while passing by the execution and it rests on a mathematical proof. The approaches is like a “Model Checking” which would apply not on a “model” but on the executable target code (interpreted). We do not carry out tests scripts but we check completely that the system follows all the the safety properties and check that the awaited functional properties did not present superfluous conditions. The SNCF developed and deposited the tools and methods making it possible industrially to carry out these treatments during the realization of the tests before put into service.
|
|
TACOS - Trustworthy Assembling of Components: frOm requirements to Specification |
|
|
|
Hassan Mountassir
LIFC & SJEPG Laboratoire d'Informatique Université de Franche-Comté 16 route de Gray 25030 Besançon
The TACOS project proposes a component-based approach to specify systems with high safety requirements. The approach concerns the first steps of the system development life-cycle, from the requirements phase to the specification phase, and aims at using or adapting existing languages and tools. Land transportation systems will be taken as an application domain. These systems, which are both distributed and embedded, require expressing functional properties as well as non functional-properties.
The project aims at answering the following questions: At the requirement level: how non-functional properties can be taken into account from the very beginning of the development life cycle? Is it possible to combine the use of context diagrams introduced by Jackson and the KAOS requirements engineering method? How to combine them with the use of UML diagrams? At the specification level: is it possible to use the B formal method with some extensions, like the addition of duration calculus, or in cooperation with other formalisms like CSP or IO interfaces automata? Some bottlenecks have been identified:
- 1. The identification of a relevant abstraction for the component expression is important. The specification of a component must include the complete information required to use it in a given context. A component can itself be defined as a combination of existing components. The information needed for the cooperation must be known. When is it possible to accept or reject the inclusion of a component in system architecture? This question is related to the interoperability problem.
- 2. The need of high level languages to model components and their assembling, from the requirement level to the specification level. These languages should be rich enough to express assembly mechanisms between components, to take into account the verification of components compatibility and interoperability. Support tools are needed for the credibility of the approach.
- 3. The chosen application domain involves embedded systems and software. Embedded systems entail time critical requirements for which very few studies have already been done. Some attempts to extend B with temporal logic allow us to address these real time specifications.
- 4. The traceability between the requirements model and the specification. Indeed, this notion of component applies to a software solution as well as to its requirements. This is still a investigation field to explore. The specification of a system consists in transforming the requirements model into a software architecture o the system. The problem is to find relevant rules that allow the translation of the elements of the requirements into elements of the system specification that form a set of well-fitted components.
The TACOS project focus on three main topics:
- - The expression of non-functional properties at the requirements level.
- - The specification of trustworthy component assembly.
- - The traceability between requirements and component specifications.
Le projet TACOS propose une approche par composants pour la spécification de systèmes sûrs, depuis l'expression des besoins jusqu'à une spécification formelle, en utilisant ou adaptant des langages et des outils existants. Le domaine d'application choisi est celui du transport. Ces systèmes, à la fois distribués et embarqués, nécessitent l'expression de propriétés fonctionnelles et non fonctionnelles.
Le projet vise à répondre aux questions suivantes : comment prendre en compte des propriétés non fonctionnelles dès les premières étapes du développement ? Comment exploiter la méthode d'analyse des besoins KAOS ? Peut-on les combiner avec l'utilisation de certains diagrammes UML ? Est-il possible d'utiliser la méthode formelle B avec des extensions et/ou en coopération avec d'autres formalismes tels que CSP ou d’autres formalismes comme les automates d’interfaces IO ? Voici quelques verrous:
- 1. L'identification de la bonne abstraction pour l'expression d'un composant est primordiale. La spécification d'un composant doit contenir les informations nécessaires pour son utilisation dans un contexte donné. Un composant peut lui-même être défini comme une combinaison de composants existants. Dans ce cas, toutes les informations nécessaires à la coopération entre les divers composants doivent être connues. Comment savoir si l'introduction d'un composant dans l'architecture d'un système peut être acceptée ou refusée ? Cette question relève du problème d'interopérabilité entre composants.
- 2. Le besoin de langages de haut niveau pour exprimer les composants et leur assemblage, depuis l'expression des besoins jusqu'à la spécification. Ces langages doivent être suffisamment riches pour exprimer des mécanismes d'assemblage entre composants et prendre en compte la vérification de la compatibilité et de l'interopérabilité. Des outils supports sont nécessaires pour la crédibilité de l'approche.
- 3. Dans le domaine d'application choisi, les aspects temps-réel sont cruciaux, aspects pour lesquels peu d'études ont été réalisées au niveau de l'expression des besoins. Quelques extensions de B avec la logique temporelle permettent d'exprimer des spécifications temps-réel.
- 4. La traçabilité entre le modèle des besoins et la spécification. La notion de composant s'applique aussi bien au niveau de la solution logicielle que de l'expression des besoins. Ce point relève encore du domaine de la recherche. La spécification d'un système consiste à transformer le modèle des besoins en une architecture de système. Le problème est de trouver des règles de transformation permettant la transformation des éléments du modèle des besoins en éléments de la spécification du système qui forment un ensemble cohérent de composants.
Le projet TACOS porte essentiellement sur trois axes:
- - L'expression de propriétés non fonctionnelles au niveau de l'expression des besoins.
- - La spécification d'un assemblage de composants digne de confiance.
- - La traçabilité entre l'expression des besoins et la spécification des composants.
|
|
MDE: from design-time to runtime |
|
|
|
|
Written by Administrator
|
Prof. Jean-Marc Jezequel
Univ. Rennes 1 & INRIA Campus de Beaulieu F-35042 RENNES (FRANCE) Tel : +33 299 847 192 Fax : +33 299 847 171 e-mail :
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
http://www.irisa.fr/prive/jezequel
Models have been used for a long time in science and engineering for managing complexity. Modeling makes it possible to separate concerns by abstracting specific aspects of reality for specific purposes. This has become quite popular in recent years to handle analysis and design concerns, leveraging modeling languages of e.g. the UML family. But separating concerns is of limited value if there is no way to compose back these concerns automatically. Automated model composition makes it easy to handle variations of design concerns, for instance in the context of maintenance or product line engineering. Beyond solving these design time issues, we show how these ideas can also be used at runtime for specifying and managing dynamically adaptive software systems, conceptualized as dynamic software product lines. We show that MDE at runtime can help engineers tame the complexity of such systems while offering a high degree of automation and validation.
IDM: du Design-time au runtime
Les modèles sont utilisés depuis longtemps en sciences et en ingénierie comme un outil fondamental de gestion de la complexité. La modélisation permet de séparer des préoccupations en abstrayant des aspects spécifiques de la réalité pour des objectifs précis. Cette approche est devenue relativement populaire ces dernières années pour faire face à des préoccupations d'analyse et de conception, en s'appuyant notamment sur des langages de modélisation de la famille d'UML. Bien sûr la séparation des préoccupations est d'un intérêt limité si on ne peut pas recomposer ses préoccupations automatiquement. La composition automatique de modèles permet en effet de gérer des variations de préoccupations de conception par exemple dans le contexte d'opérations de maintenance ou dans celui de l'ingénierie des lignes de produits. Allant au-delà de la résolution de cette problématique dans les phases de conception, nous montrons comment la composition de modèles peut aussi être utilisée pendant l'exécution d'un système pour spécifier et gérer des systèmes logiciels dynamiquement adaptatifs, ici conceptualisés comme des lignes de produits logiciels dynamiques. Montrant comment l'IDM à l'exécution peut aider les ingénieurs à maîtriser la complexité des systèmes adaptatifs tout en offrant un haut degré d'automatisation et de validation.
|
|
Applying MDE for the validation of correct Eclipse Plugin Bundles |
|
|
|
|
Written by Administrator
|
Marc Didonet del Fabro
Software Engineer, ILOG Research projects IBM Software Group 9, rue de Verdun 94253 Gentilly Cedex, France Office: +331 4908 3634 / ITN: 38723634
Complex software systems are often constructed by assembling bundles from repositiries. Eclipse is one of these systems; build on top of a platform accepting different sets of bundles according to the user needs. This adaptability is one of the main benefits of this kind of systems but implies also several configuration problems. The consistency of Eclipse plug-in’s bundles is one of them. This problem involves a need for the configuration validation. To adress this problem, this paper proposes an approach using model driven engineering. The presented solution combines different MDE techniques such as global model management and model transformations to check the coherency of Eclipse plug-in’s bundles.
Les systèmes logiciels complexes sont souvent construits par assemblage de composants provenant de différentes sources. Eclipse est un de ces systèmes, construit au dessus d’une plateforme générique acceptant différents ensembles de composants (paquets) pour s’adapter au besoin des utilisateurs. Cette adaptabilité est un des bénéfices principaux offerts par ce type ce système mais pose aussi un certain nombre de problèmes de configuration. La cohérence entre les paquets composant un système est un de ceux-ci. Cela rend nécessaire la validation de configuration. Pour résoudre ce problème, ce document propose une approche utilisant l’ingénierie dirigée par les modèles (IDM). La solution présentée combine différentes techniques utilisées en IDM comme la gestion globale de modèles et la transformation de modèles pour vérifier la cohérence du système. |
|
Flexibility in embedded real time applications : the Flex-eWare Project |
|
|
|
|
Written by Administrator
|
J. Poulou
Distributed embedded systems now widely spread in different markets: space, aircraft, manufacturing, control command as well as city monitoring and management. In the automotive domain they are used not only for monitoring and control but also for entertainment and communication. They are also used in home for entertainment and for building automation or vertical and health application, consumer electronics, etc.
Component based design is well recognized as a popular trend for embedded systems design and many approaches rely heavily on components and their composition.
Though many of theses business areas show very different requirements, especially non functional ones, we believe that numerous benefits come from bringing closer different technologies used in these areas. The Flex-eWare project targets “software flexibility” in embedded systems. It has addressed two aspects. First, the possibility to move from one technology to another one at modeling time (as a starting step) strengthens all the involved technologies. Second, architectural flexibility has been investigated in depth for different technologies and two architectural flexibility styles have been implemented.
A common component model has been defined (FCM for Flex-eWare Component Model); it is compliant with standards (UML, MARTE…) and encompasses the partner’s technologies. The FCM has been checked on five different implementation technologies and show reasonable versatility to offer a sound basis for future efforts. The availability of FCM compliant solution for tiny devices has been demonstrated, thus paving the way for seamless deployment in three third appliances involving WSN.
After reviewing these results, we conclude by outlining some coming tracks.
This work has been carried out within the Flex-eWare project granted by ANR.
Flexibilité dans les applications embarquées et temps-réel : le projet Flex-eWare
Les systèmes embarqués répartis sont omniprésents dans plusieurs types d’applications : spatial, avionique, gestion de production, automatique et contrôle, mais aussi gestion urbaine, automobile, domicile. Dans le domaine de l’automobile, il n’interviennent plus seulement dans le contrôle l’automatisation et l’aide à la conduite mais aussi pour les loisirs et la communication. Dans la maison, leurs emplois excèdent le seul domaine de la domotique pour couvrir également les loisirs (multimédia, jeux vidéo,…), l’aide à la personne et les applications de santé. L’utilisation des composants logiciels tend à prendre une part de plus en plus grande dans le développement de ces systèmes et bien des méthodes de conception reposent aujourd’hui sur les composants et la façon de les composer. Bien que de nombreux domaines d’utilisation des systèmes embarqués présentent des exigences très différentes tout particulièrement en ce qui concerne les exigences non-fonctionnelles, nous pensons que le rapprochement de technologies propres à chacun de ces domaines apporte de nombreux avantages.
Le Projet Flex-eWare vis «la flexibilité » du logiciel embarqué. Durant ce projets deux “flexibilités” particulières ont été étudiées. Tout d’abord la possibilité tout au cours du développement de déplacer un composant d’une technologie dans une autre , renforçant ainsi le domaine de pertinence des deux technologies impliquées. Ensuite, la possibilité de modifier l’architecture du logiciel en cours d’exécution a été explorée selon deux approches.
Enfin, un modèle commun de composant a été défini (FCM pour Modèle de Composant Flex-Ware). Ce modèle est compatible avec le standard actuel (UML, MARTE,…) et englobe les modèles de composants utilisés par les partenaires du projet Flex-eWare. Ce modèle a été testé sur cinq réalisations pour lesquelles il a montré des possibilités d’adaptation autorisant à le prescrire pour des futurs développements. De plus, la disponibilité d’une solution basée sur le FCM et compatibles avec de très petites cibles permet également d’envisager son utilisation dans des architectures « trois tiers » basées sur des réseaux de capteurs interconnectés par radio.
En guise de conclusion quelques perspectives sur des travaux futurs sont esquissées.
Ce travail a été réalisé dans le cadre du projet Flex-eWare subventionné par l’ANR. |
|
Applying MDE to Embedded System Design: First results and perspectives from the Lambda project |
|
|
|
|
Written by Administrator
|
S. Demathieu (Thales), Y. Bernard (Airbus), L. Maillet-Contoz, (ST Microelectronics), M. Bordin, (Adacore) F. Mallet (INRIA)
Started in June 2008, Lambda is a French collaborative research project gathering 14 partners, including industrials, SMEs and academia. The project focuses on execution platform modelling in the context of real-time embedded system design. It targets complex assemblies of COTS platforms, on test cases that are representative of system integrators' current issues (control of network latencies, tasks and scheduling configuration). A first goal is to demonstrate the technical feasibility and interest of platform modelling as a mean to validate deployment and configuration of system-level components. A second goal is to reconcile appropriate standards (SysML, MARTE, AADL, IP-XACT) with de facto standards (already implemented by widespread analysis and simulation tools).
A year and half after it started, Lambda has already provided some visible results. An extensive use of SysML/MARTE in modelling experiments has allowed the identification of good practices and of a subset of MARTE applicable within a Systems Engineering context. Key issues related to a large-scale deployment of MDE in the industry (MRO of modelling workbenches, scalability) have also started to be addressed. Concrete actions on alignment of standards (SysML, MARTE, AADL) and convergence between standards and commercial tools are leading toward a clearer standard landscape in that area.
The article describes the technical context and the issues addressed by the Lambda project. After presenting the project objectives and the partnership, it details the on-going work and presents an overview of the initial results. The article concludes with the discussion of the remaining work in the project, as well as the perspectives for the project partners.
Démarré en juin 2008, Lambda est un projet de recherche collaboratif rassemblant 14 partenaires industriels, PME et académiques. Le projet se focalise sur la modélisation de plateformes d’exécutions dans le contexte de la conception de système embarqués. Il vise des assemblages complexes de composants sur étagères, dans le cadre de cas de test représentatifs des problèmes actuels rencontrés par les intégrateurs système (contrôle de latences réseau, configuration des tâches et ordonnancement.) Un premier objectif est de démontrer la faisabilité technique, ainsi que l’intérêt, de la modélisation de plateformes, comme un moyen de valider le déploiement et la configuration des composants du systèmes. Un second objectif vise à réconcilier les standards appropriés (SysML, MARTE, AADL, IP-XACT) avec les standard de facto (déjà implémentés dans des outils d’analyse ou de simulation largement répandus).
Un an et demi après son démarrage, Lambda fourni déjà des résultats visibles. Une utilisation intensive de SysML/MARTE dans des expérimentations de modélisation a permis d’identifier des bonnes pratiques, ainsi qu’un sous-ensemble de MARTE applicable dans un contexte d’ingénierie système. Les problématiques clés liées au déploiement massif du MDE dans l’industrie (MCO des ateliers de modélisation, passage à l’échelle) ont commencé à être adressées. Des actions concrètes d’alignement des standards (SysML, MARTE, AADL) et la convergence entre standards et outil commerciaux conduit à un panorama plus clair dans ce domaine.
L’article décrit le contexte technique ainsi que les problématiques adressées par le projet Lambda. Après avoir présenté les objectifs du projet et le partenariat, il détaille les travaux en cours et présente une vue d’ensemble des premiers résultats. En conclusion, l’article évoque le travail restant dans le projet, ainsi que les perspectives pour les partenaires impliqués. |
|
Assessing quality in SysML models |
|
|
|
|
Written by Administrator
|
Olivier Casse
This e-mail address is being protected from spambots. You need JavaScript enabled to view it
“How do I know that my model is of good quality?” This question is frequently asked when developing models, and has often been asked of the authors when assisting on projects.. This is true whether developing Yourdon, IDEF0, UML, SysML, UPDM, or other modelling notations. To answer this question one needs to understand the purpose of the modelling exercise. One of the basic rules of modelling is that the purpose of the model is to fulfil a need or to answer questions. Consequently, prior to starting the modelling exercise, one has to determine the questions that need to be answered. Otherwise the model is unlikely to serve any useful purpose. For example, a model can be created from a requirements specification in order to clarify the requirements, remove inconsistency, communicate them more effectively, and ensure that they are complete, coherent, and consistent. Another model can be created from the same requirements specification that provides a means of analysing the requirements in order to specify a system or system of systems that will satisfy or realize the requirements. A third model may implement the requirements specification. This is often the case for software based systems using automatic code generation, (ACS) or Model Driven Architectures (MDA). There are a number of other possibilities such as performance modelling, simulation, behavioural modelling, human factors, etc. Other factors will also affect the scope of the model. Does the model need to capture the complete development lifecycle of the intended system – requirements through to implementation and installation? Does the model need to capture the complete lifecycle of the product – from initial concept to development, installation, maintenance and finally decommissioning? As each model has been created for a different purpose, each will have its own set of criteria for determining its level of quality. In this paper, we will first examine the concept of quality in general and as applied to modelling. For clarity there will be a brief summary of SysML in order to clarify the types of concepts that can be modelled using SysML and the typical applications for which it is used. Next we will look at the different reasons for modelling, and some of the corresponding characteristics of quality that can be applied to ensure that the model is of “good quality”. The different concepts will be illustrated with worked examples based on over 30 years of experience of modelling and implementing complex systems.
“Comment savoir si mon modèle est de bonne qualité?” cette question est fréquemment posée lors du développement de modèles et à souvent été posée aux conseillers intervenant sur les projets. Ceci est vrai que l’on développe en Yourdon, IDEF0, UML, SysML, UPDM ou toute autre notation de modélisation. Pour répondre à cette question on doit comprendre quel est l’objectif de l’exercice de modélisation. Un des principes fondamentaux de la modélisation est que le but du modèle est de satisfaire un besoin ou de répondre à des questions. En conséquence , avant de démarrer l’exercice de modélisation on doit déterminer les questions pour lesquelles nous recherchons une réponse. Sinon le modèle serait probablement inutile. Par exemple un modèle peut être créé à partir d’une spécification de façon à clarifier les exigences, ôter les incohérences, communiquer de manière plus efficace et s’assurer de sa complétude, de son uniformité et de sa cohérence. Un autre modèle peut être créé depuis les mêmes exigences qui fournira les moyens d’analyser les exigences de telle sorte à satisfaire ou à produire un système ou système de systèmes. Un troisième modèle peut implémenter la spécification. Ceci est souvent le cas pour les systèmes à logiciel prépondérant utilisant la génération de code automatique ou les techniques MDA. Il existe un certain nombre d’autres possibilités telles que la modélisation de performances, la simulation, la modélisation comportementale, les facteurs humains etc. d’autres facteurs peuvent affecter la portée du modèle. Le modèle doit il comporter le cycle de vie de développement complet du système cible – des exigences jusqu’à l’implémentation et l’installation ? le modèle doit il comporter le cycle de vie de développement complet du produit – depuis la conception initiale en passant par le développement, l’installation, la maintenance et finalement le retrait ?
Comme chaque modèle a été créé pour un objectif différent chacun aura son propre ensemble de critères afin de déterminer son niveau de qualité. Dans cet article, nous examinerons dans un premier temps le concept de qualité en général et comment l’appliquer à la modélisation. Pour plus de clarté, nous reverrons une brève introduction à SysML et ses domaines d’utilisation typiques. Ensuite nous regarderons les différentes raisons amenant à la modélisation ainsi que quelques caractéristiques de qualité pouvant être appliquées pour s’assurer que les modèle est de « bonne qualité » les différents concepts seront illustrés avec des exemples industriels basés sur plus de 30 années d’expérience de modélisation et d’implémentation de systèmes complexes |
|
Functional validation with a practical SysML / Simulink transformation |
|
|
|
|
Ray Snyder, David Bocktaels, Xavier Feigenbaum
B2i Automotive Engineering
The ever-increasing complexity of embedded systems necessitates development processes and tools to continue to meet quality, cost and delay constraints. A process built around models and the tools to construct and exploit the models are widely recognized as the principle elements of the solution. In the automotive industry Matlab/Simulink is ubiquitous for the conception and simulation of algorithms involving control and command such as found in the engine control unit. Recently, SysML has been proposed for modeling systems at a high level. SysML cannot realistically replace Simulink; it must be considered as a complementary modeling language, so a new problem is posed: of retaining a unique reference model while integrating the heterogeneous elements of SysML and the domain model.
B2i automotive engineering has implemented a development process that addresses these issues. The architecture is captured in SysML including the global behavior of the system, captured in SysML behavior diagrams. The system model is translated into a simulation ready domain model, and a test environment model is derived from the use cases. The system is then simulated in the environment to validate the functional requirements. The SysML to Simulink translation captures both the structural and behavioral elements in SysML – notably activities. Because the translation produces a ready-to-simulate model in Simulink, there is no need to conserve the latter model after the test; the SysML model remains the unique reference. We have applied this process to the development with functional validation of real industrial projects, refining the process and tools with practical experience. Simplified examples taken from these projects are used to illustrate the process.
La complexité toujours croissante des systèmes embarqués nécessite un processus de développement et des outils pour maintenir les objectifs de temps, de coût, et de qualité. La solution qui tend à s’imposer de plus en plus est l’ingénierie dirigée par des modèles en combinaison avec des outils appropriés. Dans l’industrie automobile, Matlab/Simulink est le plus répandu pour la conception et pour la simulation d’algorithmes dans le domaine du contrôle comme par exemple ceux des calculateurs de contrôle moteurs. Depuis quelques années, SysML est proposé pour la modélisation haut-niveau, toutefois SysML ne doit pas être appréhendé comme une alternative à Matlab/Simulink mais plutôt comme un complément aux activités de développement avec ce dernier. Ainsi se pose un nouveau problème, orchestrer la conception autour d’un seul modèle de référence intégrant les éléments hétérogènes de SysML et le modèle spécifique au domaine (Simulink).
Chez B2I automotive engineering, nous avons mis en place un processus pour résoudre cette problématique. SysML est utilisé pour construire l’architecture du système en y incluant son comportement global grâce aux diagrammes comportementaux de SysML. Le modèle est ensuite transformé dans un modèle simulable spécifique au domaine et dans le même temps, un modèle d’environnement, dérivé des cas d’utilisation du système. Ensuite ces modèles sont simulés ensembles pour valider les exigences fonctionnelles. La transformation de SysML vers Simulink prend en compte l’ensemble des éléments structuraux et comportementaux du modèle SysML, notamment les diagrammes d’activités. La génération automatique d’un modèle simulable complet répond à la problématique énoncée en rendant caduque le besoin d’archiver les modèles simulables. Ainsi le modèle SysML reste le modèle unique de référence.
Nous avons appliqué ce processus au développement de véritables projets. Avec l’expérience, le processus et les outils ont été améliorés. Nous montrons ici des exemples illustratifs basés sur ces développements. |
|
A SysML Based Approach to Perform FMEA |
|
|
|
Jingyi Shi1, Oliver Alt2, Wolfgang Kling2, Frank Schreiner1
1Continental Engineering Services, Graf-Vollrath-Weg 6, 60489 Frankfurt, Germany 2Continental, Business Unit Electronic Brake Systems, Guerickestraße 7, 60488 Frankfurt, Germany 1Email: {jingyi.shi, frank.schreiner}@conti-engineering.com 2Email: {oliver.alt, wolfgang.kling}@continental-corporation.com
Introduction
Since the Ford Motor Co. (USA) has applied Failure Mode Effect Analysis (FMEA) for preventive quality management in the late 1970s, the FMEA has become a widely accepted instrument for the automotive branch supporting reliable product development from early concept phase to serial production. In 1986 VDA (the Association of German Automotive Industry) published the first FMEA method description for the German automotive industry. The current FMEA method guideline is VDA 4.3. It suggests an approach to perform FMEA which consists of five steps. The first two steps “structure analysis” and “function analysis” [1] correspond to a system analysis through which the functional mechanism of the system is achieved and documented as structure tree and function structures respectively. Input for the classical FMEA forms can be derived from the system analysis. The German company APIS Informationstechnologien GmbH has developed a software product IQ-FMEA® [2] to support this procedure. This product is established as a standard tool for almost all German premium vehicle manufacturers and automotive suppliers.

Figure 1: Structure tree and function structure for FMEA [1]
Model-based development is a new approach for system and software development. In a model-based development environment a formal or semi-formal model is used to specify and define the system under development. A system may include hardware, software, information, processes, personnel, and facilities. With a system model it is possible to derive development artefacts using automation and tools. System Modelling Language (SysML) is a general-purpose modelling language for supporting model-based system development [3]. SysML offers different diagrams to describe from diverse view points the overall system context, system architecture and the behaviour of individual system components. These diagrams are usually created with appropriate tools. One of them is the software package Enterprise Architect® from SparxSystems [4].
Basic Idea
For nowadays document-centric organized development it is possible to derive the documents (including FMEA) automatically by using model-based development, assumed that the system model contains the necessary information, such as the system structure, respectively system architecture and the system behaviour. This paper presents a concept with which the FMEA documentation effort can be reduced by reusing the information out of the system model described by SysML. For a given system, the information which is needed for FMEA system analysis can already be included by system modelling using SysML, merely in another presentation form. For example the system decomposition is modelled with SysML as Block Definition Diagram, which is presented as a structure tree in FMEA. The dependency/interaction between system components can be modelled using the SysML behaviour diagrams (e.g. Sequence Diagrams, Activity Diagrams etc.) while it is presented as function structures in FMEA. Central problems of implementing this proposed concept are:
a) Which kind of modelling elements from SysML can be transformed into which kind of FMEA elements? b) What are the transformation rules? c) Can these rules be automated with help of a tool?

Figure 2: Transform SysML models to FMEA models (Concept), diagram on the left see [6]
Result and Outlook
To verify the feasibility of the above concept, a case study has been initiated and accomplished at Continental. Regarding the mentioned three problems promising results have been achieved:
1) A set of rules has been developed to transform a Block Definition Diagram, defining the system structure decomposition into a VDA 4.3 standard structure tree. 2) A method has been developed [5] to automate the transformation using the rule set. 3) Based on this method, a tool has been implemented. Using this tool, from a given Block Definition Diagram modelled in Enterprise Architect® a .xml file can be generated which can be imported as a structure tree into IQ-FMEA® for further analysis in FMEA.
Furthermore ideas have been proposed, how to realise an automated generation of VDA4.3 function structures out of the SysML models. This leads to an improved FMEA process with savings of time and money, because some development steps, done manually in the past, are now done automatically using tools.
Reference
[1] VDA Volume 4 Chapter 3: Product and Process FMEA, December 2006 [2] APIS Informationstechnologien GmbH: IQ Risk Management Tools, V5.1 Manual, 2006 [3] Tim Weilkiens. Systems Engineering with SysML/UML: Modelling, Analysis, Design. Morgan Kaufmann, 2008 [4] Sparx Systems Pty Ltd. Enterprise Architect 7.x Manual, http://www.sparxsystems.com, 2009 [5] O. Alt: Automatische Werkzeugdatenintegration mit grafischen QVT-Transformationsregeln, Proceedings of SEISCONF 2008, http://www.seisconf.org, München, 2008 [6] OMG Systems Modeling Language, The Official OMG SysML site, www.omgsysml.org, 2009
|
|