TY - GEN
T1 - Formalization and Refinement Proof for Embedded Systems
AU - Bezza, Asma
AU - Merah, Elkamel
AU - Ameur-Boulifa, Rabea
AU - Benaboud, Rohallah
AU - Messaoud Maarouk, Toufik
N1 - Publisher Copyright:
© 2020 IEEE.
PY - 2020/12/15
Y1 - 2020/12/15
N2 - This article deals with the verification of refinement of embedded systems. It's about demonstrating the correctness of the refinement engendered by transformations written in Pomset. This will allow, thereafter, the design of correct systems by construction. The principle of our formal verification approach of refinement is to benefit from the power of transition system for the formal verification. For that, we propose an algorithm allowing the passage from Pomsets to Labelled Transition system (LTS), on which we can apply algorithms of formal verification of refinement which already exist. Then, we validate our approach, applying it to the communication refinement transformation.
AB - This article deals with the verification of refinement of embedded systems. It's about demonstrating the correctness of the refinement engendered by transformations written in Pomset. This will allow, thereafter, the design of correct systems by construction. The principle of our formal verification approach of refinement is to benefit from the power of transition system for the formal verification. For that, we propose an algorithm allowing the passage from Pomsets to Labelled Transition system (LTS), on which we can apply algorithms of formal verification of refinement which already exist. Then, we validate our approach, applying it to the communication refinement transformation.
KW - Formal Methods
KW - Labelled Transition System (LTS)
KW - Pomset
KW - Proof
KW - Refinement
U2 - 10.1109/ISIA51297.2020.9416544
DO - 10.1109/ISIA51297.2020.9416544
M3 - Conference contribution
AN - SCOPUS:85106885241
T3 - ISIA 2020 - Proceedings, 4th International Symposium on Informatics and its Applications
BT - ISIA 2020 - Proceedings, 4th International Symposium on Informatics and its Applications
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 4th International Symposium on Informatics and its Applications, ISIA 2020
Y2 - 15 December 2020 through 16 December 2020
ER -