Orc is a theory of orchestration of services. It was proposed by J. Misra to model Internet-like, wide-area computations. In this project, we investigate the real-time operational semantics of Orc within the K framework using the K-tool.
We develop in this project novel extensions to sequence diagrams that reflect more accurately the control-flow structure of programs to improve program comprehension, and demonstrate the value of these extensions through case studies and experimental evaluation.
This project investigates the real-time operational semantics of Orc within the rewriting logic formalism, using Maude and its real-time extension in Real-Time Maude. The project aims at building an efficient formal analysis and verification environment for Orc programs. A propotypical implementaion for such an environment has been recently made available in the web-based tool MOrc, which is accessible online here.
An architecture-independent parallelization of the VeStA tool, in which statistical model checking of CSL/PCTL formulas and statistical quantitative analysis of formulas in QuaTEx is performed in parallel. The tool can utilize several parallel architecutres, from muti-core nodes to multi-node clusters, to significantly decrease the time required to complete these usually demanding verification tasks. The tool's web page is located here.
The formal specification and statistical model-checking and quantitative analysis of various forms of DoS attacks (such as amplification attacks) and their counter-measures, such as the Adaptive Selective Verification protocol, using Maude and PVeStA.