dc.contributor.authorDong, Jin Song
dc.contributor.authorLiu, Yang
dc.contributor.authorSun, Jun
dc.contributor.authorZhang, Xian
dc.date.accessioned2013-11-15T07:52:08Z
dc.date.available2013-11-15T07:52:08Z
dc.date.copyright2013en_US
dc.date.issued2013
dc.identifier.citationDong, J. S., Liu, Y., Sun, J., & Zhang, X. (2013). Towards verification of computation orchestration. Formal Aspects of Computing, 26(4), 729-759.en_US
dc.identifier.urihttp://hdl.handle.net/10220/17739
dc.description.abstractRecently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is no automatic verification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we define a Timed Automata semantics for the Orc language, which we prove is semantically equivalent to the operational semantics of Orc. Consequently, Timed Automata models are systematically constructed from Orc programs. The practical implication is that existing tool supports for Timed Automata, e.g., Uppaal, can be used to simulate and model check Orc programs. An experimental tool has been implemented to automate this approach. Secondly, we start with encoding the operational semantics of Orc language in Constraint Logic Programming (CLP), which allows a systematic translation from Orc to CLP. Powerful constraint solvers like CLP(R) are then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, lower or upper bound of a time interval, etc. Counterexamples are generated when properties are not satisfied. Furthermore, the stepwise execution traces can be automatically generated as the simulation steps. The two different approaches give an insight into the verification problem of Web Service orchestration. The Timed Automata approach has its merits in visualized simulation and efficient verification supported by the well developed tools. On the other hand, the CPL approach gives better expressiveness in both modeling and verification. The two approaches complement each other, which gives a complete solution for the simulation and verification of Computation Orchestration.en_US
dc.language.isoenen_US
dc.relation.ispartofseriesFormal aspects of computingen_US
dc.subjectDRNTU::Engineering::Computer science and engineering
dc.titleTowards verification of computation orchestrationen_US
dc.typeJournal Article
dc.contributor.schoolSchool of Computer Engineeringen_US
dc.identifier.doihttp://dx.doi.org/10.1007/s00165-013-0280-9


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record