Abstract: 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 and verifying complex, recursive application software will also be discussed, mostly in the context of functional programming languages (such as Haskell or Erlang).


Brief Biography of the Speaker:
Dr. Stefan D. Bruda is Associate Professor of Computer Science with Bishop's University in Sherbrooke, Quebec. He obtained his PhD from Queen's University at Kingston for his work in the area of computational models for parallel and real-time computations. His current research interests remains mostly in the theoretical realm, though they are now closer to practice being focused primarily on formal software engineering (but also on models of computation and formal languages). Since the start of his career as faculty Dr. Bruda's research has been continuously financed by the Natural Sciences and Engineering Research Council of Canada. Other financing institutions included the Fond quebecois de la recherche sur la nature et les technologies and Bishop's University. Dr. Bruda is the co-author of the book "Reconfiguration is Shared Memory: Collapsing the Hierarchy of Parallel Models with Reconfigurable Buses and Shared Memory" (LAP Publishing, 2010) and over 40 journal and conference papers. He is an editor of Parallel Processing Letters.