An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems ; Un langage intégré pour la spécification, simulation, analyse formelle et en-action des systèmes à événements discrets
In: Theses.fr, 2015
Hochschulschrift
Zugriff:
This thesis proposes a methodology which integrates formal methods in the specification, design, verification and validation processes of complex, concurrent and distributed systems with discrete events perspectives. The methodology is based on the graphical language HILLS (High Level Language for System Specification) that we defined. HiLLS integrates software engineering and system theoretic views for the specification of systems. Precisely, HiLLS integrates concepts and notations from DEVS (Discrete Event System Specification), UML (Unified Modeling Language) and Object-Z. The objectives of HILLS include the definition of a highly communicable graphical concrete syntax and multiple semantic domains for simulation, prototyping, enactment and accessibility to formal analysis. Enactment refers to the process of creating an instance of system executing in real-clock time. HILLS allows hierarchical and modular construction of discrete event systems models while facilitating the modeling process due to the simple and rigorous description of the static, dynamic, structural and functional aspects of the models. Simulation semantics is defined for HiLLS by establishing a semantic mapping between HiLLS and DEVS; in this way each HiLLS model can be simulated by a DEVS simulator. This approach allow DEVS users to use HiLLS as a modeling language in the modeling phase and use their own stand alone or distributed DEVS implementation package to simulate the models. An enactment of HiLLS models is defined by adapting the observer design-pattern to their implementation. The formal verification of HiLLS models is made by establishing morphisms between each level of abstraction of HILLS and a formal method adapted for the formal verification of the properties at this level. The formal models on which are made the formal verification are obtained from HILLS specifications by using the mapping functions. The three levels of abstraction of HILLS are: the Composite level, the Unitary level and the Traces level. These levels ...
Titel: |
An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems ; Un langage intégré pour la spécification, simulation, analyse formelle et en-action des systèmes à événements discrets
|
---|---|
Autor/in / Beteiligte Person: | Maïga, Oumar ; 2, Clermont-Ferrand ; Université des sciences, des techniques et des technologies de Bamako (Mali) ; Traoré, Mamadou Kaba ; Diallo, Ouaténi |
Link: | |
Zeitschrift: | Theses.fr, 2015 |
Veröffentlichung: | 2015 |
Medientyp: | Hochschulschrift |
Schlagwort: |
|
Sonstiges: |
|