TY - JOUR
T1 - Multi-tenant Verification-as-a-Service (VaaS) in a cloud
AU - Hu, Kai
AU - Lei, Lei
AU - Tsai, Wei Tek
N1 - Funding Information:
This work was supported by National Natural Science Foundations of China (No. 61073013 ), State Key Laboratory of Software Development Environment (No. SKLSDE-2014ZX-09 ) and Aviation Science Foundation of China (No. 2012ZC51025 ).
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
AN - SCOPUS:84946558097
SN - 1569-190X
VL - 60
SP - 122
EP - 143
JO - Simulation Modelling Practice and Theory
JF - Simulation Modelling Practice and Theory
ER -