MCaaS : Model checking in the cloud for assurances of adaptive systems
| Autor: | Andreas Metzger, Amir Molzam Sharifloo |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Model checking
business.industry Computer science Reliability (computer networking) Distributed computing 020207 software engineering System requirements specification Cloud computing 02 engineering and technology Informatik Resource (project management) Proof of concept 020204 information systems Adaptive system 0202 electrical engineering electronic engineering information engineering Key (cryptography) business |
| Zdroj: | Software Engineering for Self-Adaptive Systems III. Assurances ISBN: 9783319741826 Software Engineering for Self-Adaptive Systems |
| Popis: | Due to the uncertainty of what actual adaptations will be performed at run time, verifying adaptive systems at design time may lead to limited results or may even be infeasible. Run-time verification techniques have been proposed to cope with this uncertainty. Recently, there has been an increasing interest to use model checking (an important verification technique) at run time in order to verify the expected properties of adaptive systems. Given a system specification and expected system properties, a model checker determines whether or not the specification satisfies its properties in the presence of self-adaptation. One key concern is the generally high resource needs of model checking, which may prohibit its use on resource- and power-constrained devices, such as smart-phones or Internet-of-Things devices. To address this challenge, we introduce a cloud-based framework that delivers model checking as a service (MCaaS). MCaaS offloads computationally intensive model checking tasks to the cloud, thereby offering verification capabilities on demand. Adaptive systems running on any kind of connected device may take the advantages of model checking at run time by invoking the MCaaS service. To dynamically allocate the required cloud resources (CPU and memory), we employ machine learning to estimate the resource usage of an actual model checking task at run time. As proof of concept, we implement and validate the approach for the case of probabilistic model checking, which facilitates verifying typical properties such as reliability. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|