Méthode de conception de logiciel système critique couplée à une démarche de vérification formelle

Autor: Methni, Amira

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et po

Externí odkaz: http://www.theses.fr/2016CNAM1057/document

The synchronous Logical Execution Time paradigm

Autor: Siron, Fabien, Potop-Butucaru, Dumitru, de Simone, Robert, Chabrol, Damien, Methni, Amira

Publikováno v: ERTS 2022-Embedded real time systems
ERTS 2022-Embedded real time systems, Jun 2022, Toulouse, France

International audience; Real-Time industrial systems are not so much of those that have to perform tasks incredibly fast, but in a timepredictable manner; they rather focus on meeting previously specified timing requirements in a provable way. Conseq

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::0ae5cdd9a036d73afde07b6f4505a3ba
https://inria.hal.science/hal-03694950

Programming and verifying real-time design using logical time

Autor: Siron, Fabien, Potop-Butucaru, Dumitru, de Simone, Robert, Chabrol, Damien, Methni, Amira

Publikováno v: FDL 2021-Forum on specification & Design Languages
FDL 2021-Forum on specification & Design Languages, Sep 2021, Antibes, France

International audience; The design of embedded control software calls for stringent real-time constraints. For that, formalisms and theories based on the notion of logical time give abstraction of real-time durations that are usually not known at des

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::90f7bd8fe749d351a0707c8975dee408
https://inria.hal.science/hal-03537976/file/FDL21_paper_30.pdf

Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs

Autor: Methni, Amira, Lemerre, Matthieu, Ben Hedia, Belgacem, Haddad, Serge, Barkaoui, Kamel

Publikováno v: ICSEA 2015 The Tenth International Conference on Software Engineering Advances
Tenth International Conference on Software Engineering Advances (ISCEA 2015)
Tenth International Conference on Software Engineering Advances (ISCEA 2015), Nov 2015, Barcelone, Spain

International audience; One approach to verify the correctness of a system is to prove that it implements an executable (specification) model whose correctness is more obvious. Here, we define a kind of automata whose state is the product of values o

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::fae5d593029de2b04eb9a0caad3115f1
https://hal.archives-ouvertes.fr/hal-01501469

A method for designing critical software system coupled with a formal verification approach

Autor: Methni, Amira

Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______166::4462ca30b80a0754ac7ca143a0ecf72f
https://theses.hal.science/tel-01445983