This paper presents a tool to exploit a true concurrency model, namely the Maximality‐based Labeled Transitions Systems. We show the use of this model in model checking technique. Three techniques are implemented in order to solve the state space combinatorial explosion problem: the reduction modulo alpha‐equivalence relation, the joint use of covering steps and maximality semantics, and the maximality‐based symbolic representation.
Mots clés :
Maximality semantics
Partial order semantics
Maximality-based symbolic representation
Model checking
LOTOS specification language
Notes :
Download a free version here: https://www.researchgate.net/publication/234950656_FOCOVE_Formal_Concurrency_Verification_Environment_for_Complex_Systems
D. E. Saidouni, A. Benamira, N. Belala and F. Arfi. 2008. FOCOVE: Formal Concurrency Verification Environment for Complex Systems. In Proceedings of the 1st Mediterranean Conference on Intelligent Systems and Automation (CISA’08), Annaba, Algeria. American Institute of Physics Conference Proceedings, 1019, 1 (June 2008), American Institute of Physics, 375-380. DOI: https://doi.org/https://doi.org/10.1063/1.2953008.
APA :
Saidouni, D. E., Benamira, A., Belala, N. & Arfi, F. (2008, June). FOCOVE: Formal Concurrency Verification Environment for Complex Systems. In Proceedings of the 1st Mediterranean Conference on Intelligent Systems and Automation (CISA’08), Annaba, Algeria. American Institute of Physics Conference Proceedings, 1019(1), American Institute of Physics, 375-380. DOI: https://doi.org/https://doi.org/10.1063/1.2953008
IEEE :
D. E. Saidouni, A. Benamira, N. Belala and F. Arfi, "FOCOVE: Formal Concurrency Verification Environment for Complex Systems". In Proceedings of the 1st Mediterranean Conference on Intelligent Systems and Automation (CISA’08), Annaba, Algeria. American Institute of Physics Conference Proceedings, vol. 1019, no. 1, American Institute of Physics, pp. 375-380, June, 2008. DOI: https://doi.org/https://doi.org/10.1063/1.2953008.
BibTeX :
@inproceedings{misc-lab-202, author = {Saidouni, Djamel Eddine and Benamira, Adel and Belala, Nabil and Arfi, Farid}, title = {FOCOVE: Formal Concurrency Verification Environment for Complex Systems}, volume = {1019}, number = {1}, booktitle = {1st Mediterranean Conference on Intelligent Systems and Automation (CISA’08)}, series = {American Institute of Physics Conference Proceedings}, location = {Annaba, Algeria}, isbn = {978-0-7354-0540-0}, pages = {375--380}, publisher = {American Institute of Physics}, year = {2008}, month = {June}, doi = {https://doi.org/10.1063/1.2953008}, url = {https://aip.scitation.org/doi/abs/10.1063/1.2953008}, note = {Download a free version here: https://www.researchgate.net/publication/234950656\_FOCOVE\_Formal\_Concurrency\_Verification\_Environment\_for\_Complex\_Systems}, keywords = {Maximality semantics, Partial order semantics, Maximality-based symbolic representation, Model checking, LOTOS specification language} }
RIS :
TY - CONF TI - FOCOVE: Formal Concurrency Verification Environment for Complex Systems AU - D. E. Saidouni AU - A. Benamira AU - N. Belala AU - F. Arfi PY - 2008 VL - 1019 IS - 1 BT - 1st Mediterranean Conference on Intelligent Systems and Automation (CISA’08), Annaba, Algeria SN - 978-0-7354-0540-0 SP - 375 EP - 380 PB - American Institute of Physics AB - This paper presents a tool to exploit a true concurrency model, namely the Maximality‐based Labeled Transitions Systems. We show the use of this model in model checking technique. Three techniques are implemented in order to solve the state space combinatorial explosion problem: the reduction modulo alpha‐equivalence relation, the joint use of covering steps and maximality semantics, and the maximality‐based symbolic representation. KW - Maximality semantics KW - Partial order semantics KW - Maximality-based symbolic representation KW - Model checking KW - LOTOS specification language DO - https://doi.org/10.1063/1.2953008 UR - https://aip.scitation.org/doi/abs/10.1063/1.2953008 N1 - Download a free version here: https://www.researchgate.net/publication/234950656_FOCOVE_Formal_Concurrency_Verification_Environment_for_Complex_Systems ID - misc-lab-202 ER -