Abstract
Orchestration provides a general model of concurrent computations. A minimal yet expressive theory of orchestration is provided by Orc, in which computations are modeled by site calls and their orchestrations through a few combinators. Using Orc, formal verification of correctness of orchestrations amounts to devising an executable formal semantics of Orc and leveraging existing tool support. Despite its simplicity and elegance, giving formal semantics to Orc capturing precisely its intended behaviors is far from trivial primarily due to the challenges posed by concurrency, timing and the distinction between internal and external actions. This paper presents a semantics-based approach for formally verifying Orc orchestrations using the \({\mathbb K}\) framework. Unlike previously developed operational semantics of Orc, the \({\mathbb K}\) semantics is not directly based on the interleaving semantics given by Orc’s SOS specification. Instead, it is based on concurrent rewriting enabled by \({\mathbb K}\). It also utilizes various \({\mathbb K}\) facilities to arrive at a clean, minimal and elegant semantic specification. To demonstrate the usefulness of the proposed approach, we describe a specification for a simple robotics case study and provide initial formal verification results.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
AlTurki, M.: Rewriting-based Formal Modeling, Analysis and Implementation of Real-Time Distributed Services. PhD thesis, University of Illinois at Urbana-Champaign (August 2011), http://hdl.handle.net/2142/26231
AlTurki, M.A., Meseguer, J.: Executable rewriting logic semantics of Orc and formal analysis of Orc programs. Journal of Logical and Algebraic Methods in Programming (to appear, 2015)
Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comput. Sci. 96(1), 217–248 (1992)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Cook, W.R., Patwardhan, S., Misra, J.: Workflow patterns in Orc. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 82–96. Springer, Heidelberg (2006)
Şerbănuţă, T.F., Arusoaie, A., Lazar, D., Ellison, C., Lucanu, D., Roşu, G.: The \(\mathbb{K}\) primer (version 3.3). In: Hills, M. (ed.) Proceedings of the Second International Workshop on the \(\mathcal{K}\) Framework and its Applications (\(\mathcal{K}\) 2011), vol. 304, pp. 57–80. Elsevier (2014)
Şerbănuţă, T.F., Roşu, G.: A truly concurrent semantics for the \(\mathbb{K}\) framework based on graph transformations. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 294–310. Springer, Heidelberg (2012)
Şerbănuţă, T.F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Information and Computation 207(2), 305–340 (2009); Special issue on Structural Operational Semantics (SOS)
Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 533–544. ACM, Philadelphia (2012)
Farzan, A., Chen, F., Meseguer, J., Roşu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501–505. Springer, Heidelberg (2004)
Farzan, A., Meseguer, J., Roşu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 132–147. Springer, Heidelberg (2004)
Kitchin, D., Powell, E., Misra, J.: Simulation using orchestration. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 2–15. Springer, Heidelberg (2008)
Kitchin, D., Quark, A., Misra, J.: Quicksort: Combining concurrency, recursion, and mutable data structures. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, History of Computing, pp. 229–254. Springer, London (2010)
Lazar, D., Arusoaie, A., Şerbǎnuţǎ, T.F., Ellison, C., Mereuta, R., Lucanu, D., Roşu, G.: Executing formal semantics with the \(\mathbb{K}\) tool. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 267–271. Springer, Heidelberg (2012)
Lucanu, D., Şerbănuţă, T.F., Roşu, G.: \(\mathbb{K}\) framework distilled. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 31–53. Springer, Heidelberg (2012)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Meseguer, J., Roşu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373(3), 213–237 (2007)
Meseguer, J., Roşu, G.: The rewriting logic semantics project: A progress report. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 1–37. Springer, Heidelberg (2011)
Misra, J.: Computation orchestration: A basis for wide-area computing. In: Broy, M. (ed.) Proc. of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems. NATO ASI Series, Marktoberdorf, Germany (2004)
Misra, J.: Structured concurrent programming. Manuscript, University of Texas at Austin (December 2014), http://www.cs.utexas.edu/users/misra/temporaryFiles.dir/Orc.pdf
Misra, J., Cook, W.R.: Computation orchestration. Software and Systems Modeling 6(1), 83–110 (2007)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)
Roşu, G., Şerbănuţă, T.F.: An overview of the \(\mathbb{K}\) semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010); Membrane computing and programming
Roşu, G., Şerbănuţă, T.F.: \(\mathbb{K}\) overview and SIMPLE case study. In: Hills, M. (ed.) Proceedings of the Second International Workshop on the \(\mathbb{K}\) Framework and its Applications (\(\mathbb{K}\) 2011). Electronic Notes in Theoretical Computer Science, vol. 304, pp. 3–56. Elsevier (2014)
Wehrman, I., Kitchin, D., Cook, W.R., Misra, J.: A timed semantics of Orc. Theoretical Computer Science 402(2- 3), 234–248 (2008); Trustworthy Global Computing
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
AlTurki, M.A., Alzuhaibi, O. (2015). Towards Formal Verification of Orchestration Computations Using the \({\mathbb K}\) Framework. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-19249-9_4
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19248-2
Online ISBN: 978-3-319-19249-9
eBook Packages: Computer ScienceComputer Science (R0)