Abstract
Modern software systems are highly configurable and evolve over time. Simultaneously, they have high demands on their correctness and trustworthiness. Formal verification technique are a means to ensure critical system requirements, but still require a lot of computation power and manual intervention. In this paper, we argue that formal verification processes can be cast as workflows known from business process modeling. Single steps in the verification process constitute verification tasks which can be flexibly combined to verification workflows. The verification tasks can be carried out using designated services which are provided by highly scalable computing platforms, such as cloud computing environments. Verification workflows share the characteristics of business processes such that well-established results and tool support from workflow modeling, management and analysis are directly applicable. System evolution causing re-verification is supported by workflow adaptation techniques such that previously established verification results can be reused.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Adler, R., Schaefer, I., Schuele, T., Vecchié, E.: From Model-Based Design to Formal Verification of Adaptive Embedded Systems. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 76–95. Springer, Heidelberg (2007)
Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Ruess, H., Rushby, J., Rusu, V., Saidi, H., Shankar, N., Singerman, E., Tiwari, A.: An Overview of SAL. In: Fifth NASA Langley Formal Methods Workshop (LFM), pp. 187–196 (2000)
Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF Toolset. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 237–267. Springer, Heidelberg (2004)
Clarke, E., Grumberg, O., Long, D.: Model Checking and Abstraction. ACM Trans. Prog. Lang. Syst. 16(5), 1512–1542 (1994)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Hollingsworth, D.: The workflow reference model. Technical report, WfMC, Document TC-1003 (1995)
Kupferman, O., Vardi, M.: Modular Model Checking. In: Compositionality: The Significant Difference, Int’l Symposium, pp. 381–401 (1997)
Lamprecht, A.-L., Margaria, T., Steffen, B.: Bio-jETI: a framework for semantics-based service composition. BMC Bioinformatics (2009)
Ludäscher, B., Altintas, I., Berkley, C., Higgins, D., Jaeger, E., Jones, M., Lee, E.A., Tao, J., Zhao, Y.: Scientific workflow management and the kepler system. Concurrency and Computation: Practice & Experience 18, 1039–1065 (2006)
Sauer, T., Minor, M., Bergmann, R.: Inverse workflows for supporting agile business process management. In: Proceedings of the 6th Conference on Professional Knowledge Management. LNI, vol. 182, pp. 204–213 (2011)
Schaefer, I.: Integrating Formal Verification into the Model-based Development for Adaptive Embedded Systems. PhD thesis, University of Kaiserslautern (2008)
Schaefer, I., Hähnle, R.: Formal methods in software product line engineering. IEEE Computer 44(2), 82–85 (2011)
van der Aalst, W.M.P., van Hee, K.: Workflow Management: Models, Methods and Systems. MIT Press (2002)
Wei, Y., Blake, M.B.: Service-oriented computing and cloud computing: Challenges and opportunities. IEEE Internet Computing 14(6), 72–75 (2010)
Zhang, L.-J., Zhang, J., Cai, H.: Services Computing. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schaefer, I., Sauer, T. (2012). Towards Verification as a Service. In: Moschitti, A., Scandariato, R. (eds) Eternal Systems. EternalS 2011. Communications in Computer and Information Science, vol 255. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28033-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-28033-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28032-0
Online ISBN: 978-3-642-28033-7
eBook Packages: Computer ScienceComputer Science (R0)