Design for Verifiability: The OCS Case Study
Johannes Neubauer, Tiziana Margaria, Bernhard Steffen · Formal Methods for Industrial Critical Systems · 2012
This chapter focuses on the verification, validation, and in particular the learning aspects, and treat the complex semiautomatic transformation process, which takes care of: process synchronization via messages; event handling via messages; parallelism via (dynamically created) threads (shared resources); and persistence of the process state and business objects, as a “black box”. More concretely, the chapter describes how the “local” models of the Online Conference System (OCS) are developed and verified, and how their combination to a system running on an enterprise platform can be validated. Key to the global validation of the corresponding emergent behavior is the experimental exploration of and behavioral model construction for the system via automata learning. Subsequently, the chapter sketches how this approach might scale, summarize related work, and finally present our conclusions and perspectives. Controlled Vocabulary Terms automata theory