Abstract
Modern enterprise information systems are built following the paradigm of service-orientation. This paradigm promotes workflow-based software composition, where complex business processes are realized by orchestrating different, heterogenous components. These workflow descriptions evolve continuously, to adapt to changes in the business goals or in the enterprise policies. Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial.
In this paper we focus on the probabilistic verification of reliability requirements of structured workflows. We propose a novel incremental technique based on a syntactic-semantic approach. Reliability analysis is driven by the syntactic structure (defined by an operator-precedence grammar) of the workflow and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. The approach has been implemented in a prototype tool; preliminary experimental evaluation confirms the theoretical speedup over a nonincremental approach.
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
van der Aalst, W.M.P., Ter Hofstede, A.H.M., Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distrib. Parallel Databases 14(1), 5–51 (2003)
Avizienis, A., Laprie, J.-C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secure Comput. 1(1), 11–33 (2004)
Barenghi, A., Viviani, E., Crespi Reghizzi, S., Mandrioli, D., Pradella, M.: PAPAGENO: A parallel parser generator for operator precedence grammars. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol. 7745, pp. 264–274. Springer, Heidelberg (2013)
Baresi, L., Di Nitto, E., Ghezzi, C.: Toward open-world software: Issues and challenges. IEEE Computer 39(10), 36–43 (2006)
Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: A syntactic-semantic approach to incremental verification (2013), http://arxiv.org/abs/1304.8034
Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: Syntactic-semantic incrementality for agile verification. Sci. Comput. Program (2013), doi:10.1016/j.scico.2013.11.026
Borges, M., Filieri, A., d’Amorim, M., Păsăreanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: Proc. of PLDI 2014, pp. 123–132. ACM (2014)
de Bosschere, K.: An operator precedence parser for standard Prolog text. Softw. Pract. Exper. 26(7), 763–779 (1996)
Cheung, R.C.: A user-oriented software reliability model. IEEE Trans. Softw. Eng. SE-6(2), 118–125 (1980)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Reghizzi, S.C., Mandrioli, D.: Operator precedence and the visibly pushdown property. J. Comput. Syst. Sci. 78(6), 1837–1867 (2012)
Daws, C.: Symbolic and parametric model checking of discrete-time markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005)
Distefano, S., Ghezzi, C., Guinea, S., Mirandola, R.: Dependability assessment of web service orchestrations. IEEE Trans. Rel. (2014) (PrePrint), doi:10.1109/TR.2014.2315939
Distefano, S., Filieri, A., Ghezzi, C., Mirandola, R.: A compositional method for reliability analysis of workflows affected by multiple failure modes. In: Proc. of CBSE 2011, pp. 149–158. ACM (2011)
Ershov, A.: On the partial computation principle. Inform. Process. Lett. 6(2), 38–41 (1977)
Filieri, A., Ghezzi, C.: Further steps towards efficient runtime verification: Handling probabilistic cost models. In: Proc. of FormSERA 2012, pp. 2–8. IEEE (2012)
Filieri, A., Păsăreanu, C.S., Visser, W., Geldenhuys, J.: Statistical symbolic execution with informed sampling. In: Proc. of SIGSOFT 2014/FSE-22, ACM (2014)
Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Proc. of ICSE 2011, pp. 341–350. ACM (2011)
Filieri, A., Ghezzi, C., Tamburrelli, G.: A formal approach to adaptive software: continuous assurance of non-functional requirements. Formal Asp. Comput. 24(2), 163–186 (2012)
Filieri, A., Păsăreanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: Proc. of ICSE 2013, pp. 622–631. IEEE Press (2013)
Floyd, R.W.: Syntactic analysis and operator precedence. J. ACM 10, 316–333 (1963)
Gallotti, S., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Quality prediction of service compositions through probabilistic model checking. In: Becker, S., Plasil, F., Reussner, R. (eds.) QoSA 2008. LNCS, vol. 5281, pp. 119–134. Springer, Heidelberg (2008)
Ghezzi, C.: Evolution, adaptation, and the quest for incrementality. In: Calinescu, R., Garlan, D. (eds.) Monterey Workshop 2012. LNCS, vol. 7539, pp. 369–379. Springer, Heidelberg (2012)
Ghezzi, C., Mandrioli, D.: Incremental parsing. ACM Trans. Program. Lang. Syst. 1(1), 58–70 (1979)
Goseva-Popstojanova, K., Mathur, A., Trivedi, K.: Comparison of architecture-based software reliability models. In: Proc. of ISSRE 2001, pp. 22–31. IEEE (2001)
Grune, D., Jacobs, C.J.H.: Parsing Techniques - a practical guide, 2nd edn. Springer (2008)
Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. STTT 13(1), 3–19 (2011)
Immonen, A., Niemela, E.: Survey of reliability and availability prediction methods from the viewpoint of software architecture. Software and Systems Modeling 7(1), 49–65 (2008)
Johnson, K., Calinescu, R., Kikuchi, S.: An incremental verification framework for component-based software systems. In: Proc. of CBSE 2013, pp. 33–42. ACM (2013)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)
Josuttis, N.: SOA in Practice: The Art of Distributed System Design. O’Reilly (2007)
Knuth, D.E.: Semantics of context-free languages. Theory of Computing Systems 2, 127–145 (1968)
Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: Proc. of DSN 2011, pp. 359–370. IEEE (2011)
Meedeniya, I., Grunske, L.: An efficient method for architecture-based reliability evaluation for evolving systems with changing parameters. In: Proc. of ISSRE 2010, pp. 229–238. IEEE (2010)
Pham, H.: System software reliability. Springer (2006)
Sistla, P.: Hybrid and incremental model-checking techniques. ACM Comput. Surv. 28(4es) (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D. (2014). Incremental Syntactic-Semantic Reliability Analysis of Evolving Structured Workflows. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2014. Lecture Notes in Computer Science, vol 8802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45234-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-45234-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45233-2
Online ISBN: 978-3-662-45234-9
eBook Packages: Computer ScienceComputer Science (R0)