Skip to Main content Skip to Navigation
Theses

Aide à la réutilisation de spécifications formelles en LOTOS

Abstract : Reuse is a key to improve the quality and the productivity of software. However, there are still problems not entirely resolved limiting the practice of reuse such as construction of a reusable component and adaptation of a component in an application according to the specific needs of the user. In our work, we are interested to the reuse of formal specifications. These specifications allow on one hand a system description to de more abstract, explicit and modular than the code and on the other hand to prove the correction of new system. We focused on two specifications types : abstract data types and concurrent processes using LOTOS language. To support specification reuse, we defined new and complex methods : re-striction, promotion and generalization of data types as well a composition and extension of processes. These methods are aided with operators defined in Proplane model. Reuse operators are based on theories (to produce correct results), are automatic ( the users are not necessarily experts in formal methods) and interactive (to support the user intuition). We applied these operators on case studies.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2000_0030_SADAOUI_MOUHOUB.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01746434
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:37:46 AM
Last modification on : Wednesday, December 16, 2020 - 3:32:51 PM

Identifiers

  • HAL Id : tel-01746434, version 1

Collections

Citation

Samira Sadaoui-Mouhoub. Aide à la réutilisation de spécifications formelles en LOTOS. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2000. Français. ⟨NNT : 2000NAN10030⟩. ⟨tel-01746434⟩

Share

Metrics

Record views

19