Multi-tenant Verification-as-a-Service (VaaS) in a cloud

Kai Hu, Lei Lei, Wei Tek Tsai

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

Formal methods and verification technique are often used to develop mission-critical systems. Cloud computing offers new computation models for applications and the new model can be used for formal verification. But formal verification tools and techniques may need to be updated to exploit the cloud architectures. Multi-Tenant Architecture (MTA) is a design architecture used in SaaS (Software-as-a-Service) where a tenant can customize its applications by integrating either services already stored in the SaaS database or newly supplied services. This paper proposes a new concept VaaS (Verification-as-a-Service), similar to SaaS, by leveraging the computing power offered by a cloud environment with automated provisioning, scalability, and service composition. A VaaS hosts verification software in a cloud environment, and these services can be called on demand, and can be composed to verify a software model. This paper presents a VaaS architecture with components, and ways that a VaaS can be used to verify models. Bigragh is selected as the modeling language for illustration as it can model mobile applications. A Bigraph models can be verified by first converting it to a state model, and the state model can be verified by model-checking tools. The VaaS services combination model and execution model are also presented. The algorithm of distributing VaaS services to a cloud is given and its efficiency is evaluated. A case study is used to demonstrate the feasibility of a VaaS.

Original languageEnglish (US)
Pages (from-to)122-143
Number of pages22
JournalSimulation Modelling Practice and Theory
Volume60
DOIs
StatePublished - Jan 1 2016

Fingerprint

Software-as-a-Service
Formal Verification
Model
Formal methods
Verify
Model checking
Software Verification
Cloud computing
Mobile Applications
Service Composition
Formal Methods
Scalability
Modeling Language
Cloud Computing
Model Checking
Chemical analysis
Software
Architecture
Computing
Formal verification

Keywords

  • Bigraph
  • Formal method
  • Model checking
  • Multi-Tenant Architecture (MTA)
  • SaaS
  • Verification-as-a-Service (VaaS)

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software
  • Modeling and Simulation

Cite this

Multi-tenant Verification-as-a-Service (VaaS) in a cloud. / Hu, Kai; Lei, Lei; Tsai, Wei Tek.

In: Simulation Modelling Practice and Theory, Vol. 60, 01.01.2016, p. 122-143.

Research output: Contribution to journalArticle

Hu, Kai ; Lei, Lei ; Tsai, Wei Tek. / Multi-tenant Verification-as-a-Service (VaaS) in a cloud. In: Simulation Modelling Practice and Theory. 2016 ; Vol. 60. pp. 122-143.
@article{3cb422c9897743d59ad2e73eac958bcd,
title = "Multi-tenant Verification-as-a-Service (VaaS) in a cloud",
abstract = "Formal methods and verification technique are often used to develop mission-critical systems. Cloud computing offers new computation models for applications and the new model can be used for formal verification. But formal verification tools and techniques may need to be updated to exploit the cloud architectures. Multi-Tenant Architecture (MTA) is a design architecture used in SaaS (Software-as-a-Service) where a tenant can customize its applications by integrating either services already stored in the SaaS database or newly supplied services. This paper proposes a new concept VaaS (Verification-as-a-Service), similar to SaaS, by leveraging the computing power offered by a cloud environment with automated provisioning, scalability, and service composition. A VaaS hosts verification software in a cloud environment, and these services can be called on demand, and can be composed to verify a software model. This paper presents a VaaS architecture with components, and ways that a VaaS can be used to verify models. Bigragh is selected as the modeling language for illustration as it can model mobile applications. A Bigraph models can be verified by first converting it to a state model, and the state model can be verified by model-checking tools. The VaaS services combination model and execution model are also presented. The algorithm of distributing VaaS services to a cloud is given and its efficiency is evaluated. A case study is used to demonstrate the feasibility of a VaaS.",
keywords = "Bigraph, Formal method, Model checking, Multi-Tenant Architecture (MTA), SaaS, Verification-as-a-Service (VaaS)",
author = "Kai Hu and Lei Lei and Tsai, {Wei Tek}",
year = "2016",
month = "1",
day = "1",
doi = "10.1016/j.simpat.2015.09.003",
language = "English (US)",
volume = "60",
pages = "122--143",
journal = "Simulation Modelling Practice and Theory",
issn = "1569-190X",
publisher = "Elsevier",

}

TY - JOUR

T1 - Multi-tenant Verification-as-a-Service (VaaS) in a cloud

AU - Hu, Kai

AU - Lei, Lei

AU - Tsai, Wei Tek

PY - 2016/1/1

Y1 - 2016/1/1

N2 - Formal methods and verification technique are often used to develop mission-critical systems. Cloud computing offers new computation models for applications and the new model can be used for formal verification. But formal verification tools and techniques may need to be updated to exploit the cloud architectures. Multi-Tenant Architecture (MTA) is a design architecture used in SaaS (Software-as-a-Service) where a tenant can customize its applications by integrating either services already stored in the SaaS database or newly supplied services. This paper proposes a new concept VaaS (Verification-as-a-Service), similar to SaaS, by leveraging the computing power offered by a cloud environment with automated provisioning, scalability, and service composition. A VaaS hosts verification software in a cloud environment, and these services can be called on demand, and can be composed to verify a software model. This paper presents a VaaS architecture with components, and ways that a VaaS can be used to verify models. Bigragh is selected as the modeling language for illustration as it can model mobile applications. A Bigraph models can be verified by first converting it to a state model, and the state model can be verified by model-checking tools. The VaaS services combination model and execution model are also presented. The algorithm of distributing VaaS services to a cloud is given and its efficiency is evaluated. A case study is used to demonstrate the feasibility of a VaaS.

AB - Formal methods and verification technique are often used to develop mission-critical systems. Cloud computing offers new computation models for applications and the new model can be used for formal verification. But formal verification tools and techniques may need to be updated to exploit the cloud architectures. Multi-Tenant Architecture (MTA) is a design architecture used in SaaS (Software-as-a-Service) where a tenant can customize its applications by integrating either services already stored in the SaaS database or newly supplied services. This paper proposes a new concept VaaS (Verification-as-a-Service), similar to SaaS, by leveraging the computing power offered by a cloud environment with automated provisioning, scalability, and service composition. A VaaS hosts verification software in a cloud environment, and these services can be called on demand, and can be composed to verify a software model. This paper presents a VaaS architecture with components, and ways that a VaaS can be used to verify models. Bigragh is selected as the modeling language for illustration as it can model mobile applications. A Bigraph models can be verified by first converting it to a state model, and the state model can be verified by model-checking tools. The VaaS services combination model and execution model are also presented. The algorithm of distributing VaaS services to a cloud is given and its efficiency is evaluated. A case study is used to demonstrate the feasibility of a VaaS.

KW - Bigraph

KW - Formal method

KW - Model checking

KW - Multi-Tenant Architecture (MTA)

KW - SaaS

KW - Verification-as-a-Service (VaaS)

UR - http://www.scopus.com/inward/record.url?scp=84946558097&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84946558097&partnerID=8YFLogxK

U2 - 10.1016/j.simpat.2015.09.003

DO - 10.1016/j.simpat.2015.09.003

M3 - Article

VL - 60

SP - 122

EP - 143

JO - Simulation Modelling Practice and Theory

JF - Simulation Modelling Practice and Theory

SN - 1569-190X

ER -