Cyber-Physical Systems (CPSs) are engineered systems that are built from, and depend upon, the seamless integration of computational algorithms and physical components. CPSs are widely used in many safety-critical domains, making it crucial to ensure that they operate safely without causing harm to people and the environment. Therefore, their design should be robust enough to deal with unexpected conditions and flexible to answer to the high scalability and complexity of systems. Nowadays, it is well-established that formal verification has a great potential in reinforcing safety of critical systems, but nevertheless its application in the development of industrial products may still be a challenging activity. In this paper, we describe an approach based on Satisfiability Modulo Theories (SMT) to formally verify, at the design stage, the consistency of the system design – expressed in a given domain-specific language, called QRML, which is specifically designed for CPSs – with respect to some given property constraints, with the purpose to reduce inconsistencies during the system development process. To this end, we propose an SMT-based approach for checking the consistency of configuration based-components specifications and we report the results of the experimental analysis using three different state-of-the-art SMT solvers. The main goal of the experimental analysis is to test the scalability of the selected SMT solvers and thus to determine which SMT solver is the best in checking the satisfiability of the properties.

SMT-Based Consistency Checking of Configuration-Based Components Specifications / Pandolfo, L.; Pulina, L.; Vuotto, S.. - In: IEEE ACCESS. - ISSN 2169-3536. - 9:(2021), pp. 83718-83726. [10.1109/ACCESS.2021.3085911]

SMT-Based Consistency Checking of Configuration-Based Components Specifications

Pandolfo L.
;
Pulina L.
;
Vuotto S.
2021-01-01

Abstract

Cyber-Physical Systems (CPSs) are engineered systems that are built from, and depend upon, the seamless integration of computational algorithms and physical components. CPSs are widely used in many safety-critical domains, making it crucial to ensure that they operate safely without causing harm to people and the environment. Therefore, their design should be robust enough to deal with unexpected conditions and flexible to answer to the high scalability and complexity of systems. Nowadays, it is well-established that formal verification has a great potential in reinforcing safety of critical systems, but nevertheless its application in the development of industrial products may still be a challenging activity. In this paper, we describe an approach based on Satisfiability Modulo Theories (SMT) to formally verify, at the design stage, the consistency of the system design – expressed in a given domain-specific language, called QRML, which is specifically designed for CPSs – with respect to some given property constraints, with the purpose to reduce inconsistencies during the system development process. To this end, we propose an SMT-based approach for checking the consistency of configuration based-components specifications and we report the results of the experimental analysis using three different state-of-the-art SMT solvers. The main goal of the experimental analysis is to test the scalability of the selected SMT solvers and thus to determine which SMT solver is the best in checking the satisfiability of the properties.
SMT-Based Consistency Checking of Configuration-Based Components Specifications / Pandolfo, L.; Pulina, L.; Vuotto, S.. - In: IEEE ACCESS. - ISSN 2169-3536. - 9:(2021), pp. 83718-83726. [10.1109/ACCESS.2021.3085911]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11388/247737
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact