Orchestrating with Contracts

Our domain of interest is self-healing systems. We wish to reason about the behavior of statically and dynamically composed systems. The orchestration language Orc permits one to write programs that compose such systems. Unfortunately, Orc's semantics make no assumptions about the behavior of the units under composition. Orc is an executable language, and in the Orc system, units are realized as methods implemented in the Java programming language. Since Java methods' behavior can be formally specified with the Java Modeling Language (JML), then the behavior of an Orc program can be reasoned about via a synthesis of the semantics of Orc and JML.