Plenary lecture 4: engineering application software: a formal primer
Stefan D. Bruda · 2010
Formal methods-be they logical (such as model checking) or algebraic (such as model-based testing)- have established themselves as mainstream tools for verification and validation. Hardware, device drivers, and network protocol have all been formally validated in various contexts. Recent Turing prizes have recognized this success. When it comes to specifying and verifying complex application software, formal methods have hit however a stumbling block. Indeed, conformance testing is traditionally based on finite-state formalisms: a system is at any time in one of the multitude of named states. Such an approach fails for complex software because of the sheer number of necessarily distinct states (already happening in simpler systems, but becoming simply unmanageable for complex applications such as word processors or operating systems). Bringing conformance testing to complex application software is an emerging area. Typical programming languages (and thus the control flow of software programmed using them) feature nested, recursive invocations of program modules. These features are modelled naturally by context-free languages. Many non-regular properties are therefore required for software verification. Such properties generate an finite state space, which cannot be handled by finite-state process algebrae or by standard verification techniques such as model checking. Context-free process algebrae such as BPA can specify context-free properties. However, concurrency cannot be provided by context-free process algebrae since context-free languages are not closed under intersection. This talk focuses on the quest of finding a formalism that is expressive enough to model the context-free phenomenae from complex software yet allows for a compositional approach to conformance testing. We start with visibly pushdown languages (VPL), a promising construct which unfortunately is not suitable for compositional specification and verification. We extend VPL to multiple stacks, obtaining multi-stack visibly pushdown languages (MVPL). These languages model concurrency naturally, but their standard definition does not allow compositional approaches. We then present an alternate set of operations over MVPL that are natural and also permit compositional specification and verification. The subsequent tools for specifying complex, recursive application software will also be discussed.