SMT-Based Consistency Checking of Configuration-Based Components Specifications
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2021-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9446129/ |
| _version_ | 1819063918348206080 |
|---|---|
| author | Laura Pandolfo Luca Pulina Simone Vuotto |
| author_facet | Laura Pandolfo Luca Pulina Simone Vuotto |
| author_sort | Laura Pandolfo |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-21T15:22:18Z |
| format | Article |
| id | doaj.art-c5e04de964af4ca2b318868916607f85 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-21T15:22:18Z |
| publishDate | 2021-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-c5e04de964af4ca2b318868916607f852022-12-21T18:59:00ZengIEEEIEEE Access2169-35362021-01-019837188372610.1109/ACCESS.2021.30859119446129SMT-Based Consistency Checking of Configuration-Based Components SpecificationsLaura Pandolfo0https://orcid.org/0000-0002-5785-5638Luca Pulina1https://orcid.org/0000-0003-0258-3222Simone Vuotto2Intelligent System Design and Applications (IDEA) Laboratory, University of Sassari, Sassari, ItalyIntelligent System Design and Applications (IDEA) Laboratory, University of Sassari, Sassari, ItalyIntelligent System Design and Applications (IDEA) Laboratory, University of Sassari, Sassari, ItalyCyber-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.https://ieeexplore.ieee.org/document/9446129/Design verificationapplication of formal methodssatisfiability modulo theories |
| spellingShingle | Laura Pandolfo Luca Pulina Simone Vuotto SMT-Based Consistency Checking of Configuration-Based Components Specifications IEEE Access Design verification application of formal methods satisfiability modulo theories |
| title | SMT-Based Consistency Checking of Configuration-Based Components Specifications |
| title_full | SMT-Based Consistency Checking of Configuration-Based Components Specifications |
| title_fullStr | SMT-Based Consistency Checking of Configuration-Based Components Specifications |
| title_full_unstemmed | SMT-Based Consistency Checking of Configuration-Based Components Specifications |
| title_short | SMT-Based Consistency Checking of Configuration-Based Components Specifications |
| title_sort | smt based consistency checking of configuration based components specifications |
| topic | Design verification application of formal methods satisfiability modulo theories |
| url | https://ieeexplore.ieee.org/document/9446129/ |
| work_keys_str_mv | AT laurapandolfo smtbasedconsistencycheckingofconfigurationbasedcomponentsspecifications AT lucapulina smtbasedconsistencycheckingofconfigurationbasedcomponentsspecifications AT simonevuotto smtbasedconsistencycheckingofconfigurationbasedcomponentsspecifications |