A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements Using TASTD

• Alex Rodrigue Ndouna Université de Sherbrooke https://orcid.org/0009-0004-1996-2434
• Marc Frappier Université de Sherbrooke https://orcid.org/0000-0002-4402-2514
• Frédéric Mallet Université Côte d'Azur https://orcid.org/0000-0002-9088-9821

Resumo

Designing and verifying safety-critical systems requires giving equal importance to non-functional and functional requirements from the start, especially those related to time. Since no single method can address all system aspects, a combination of formal methods is needed for accurate modeling and analysis. This paper proposes an integration of the CCSL (Clock constraints Specification language) and TASTD specification languages for the modular modeling of timing requirements. CCSL allows for the modular expression of timing constraints, whereas TASTD allows for the combination of state machines using CSP process algebra operators, to foster the construction of a system specification using the composition of small components specification. We propose rules to translate a CCSL specification into a TASTD specification, which can use the CSP [14] operators of TASTD to compose the CCSL constraints with other specification elements, like operating modes of a system. The CCSL part of the specification can be verified using CCSL tools. The global specification can be simulated using TASTD tools. The approach is demonstrated on a temperature control system which has been previously modeled using UML MARTE and CCSL, but for which no formal combination was available.

Palavras-chave: ASTD, CCSL, TASTD, formal methods