In 1999 three formal-methods researchers, including the speaker, founded a company to commercializeformal modeling and verification technology for envisioned telecommunications customers. Eight years later, the company sells testing tools to embedded control software developers in the automotive, aerospace and related industries. This talk will describe the journey taken by the company during its evolution, why this journey was both less and more far than it seems, and how the speaker's views on practical utility of mathematically oriented software research changed along the way.
In spite of cultural difference between the corresponding scientific communities, recognition is growing that test-based and specification-based approaches to software development actually complement each other. The revival of interest in testing tools and techniques follows in particular from the popularity of "Test-Driven Development"; rigorous specification and proofs have, for their part, also made considerable progress. There remains, however, a fundamental superiority of specifications over test: you can derive tests from a specification, but not the other way around. Contract-Driven Development is a new approach to systematic software construction combining ideas from Design by Contract, from Test-Driven Development, from work on formal methods, and from advances in automatic testing as illustrated for example in our AutoTest tool. Like TDD it gives tests a central role in the development process, but these tests are deduced from possibly partial specifications (contracts) and directly supported by the development environment. This talk will explain the concepts and demonstrate their application.
Program refactoring, feature-based and aspect-oriented software synthesis, and model-driven development are disjoint research areas. However, they are all architectural metaprogramming technologies as they treat programs as values and use functions (a.k.a. transformations) to map programs to other programs. In this presentation, I explore their underlying connections by reviewing recent advances in each area from an architectural metaprogramming perspective. I conjecture how these areas can converge and outline a theory that may unify them.
Two phrases in a programming language are said to be contextually equivalent if, roughly speaking, they are interchangeable in any complete program without affecting the observable behaviour of the program. I will discuss precise formalisations of this fundamental notion of semantic equivalence for the case of higher-order, typed (HOT) languages, such as ML and Haskell. How does the structure of a type affect properties of contextual equivalence of expressions of that type? It can be very difficult to answer this question when working directly from the definition of contextual equivalence---mainly because HOT programs can make use of their constituent sub-expressions in dynamically complicated ways. This talk will survey some of the semantic techniques (both denotational and operational) that have been devised for proving properties of HOT contextual equivalence.
Software product families have found broad adoption in the embedded systems industry. During recent years, however, companies have started to stretch the scope of their product families significantly beyond the initial scope, in response to several trends, including convergence, end-to-end solutions, shortened innovation and R&D cycles and differentiaton through software engineering capabilities. At the same time, companies have failed to align their approach to product families in response to changes in the business strategy, leading to several challenging problems that can be viewed as symptoms of this approach. This talk presents compositional product families as solution to these challenges and outlines the strategic, technical and process and organizational aspects of the approach.
Aspects have emerged as a powerful tool in the design and development
of systems. Aspect-orientation ideas are paradigm independent
and have been developed for object-oriented, imperative and functional
This talk will discuss a suite of results that aim to level the foundational playing field between aspects and other programming paradigms. In this context, we will argue that aspects are no more intractable than stateful higher order programs.
The Talk is based on joint work with Glenn Bruns, Alan Jeffrey, Corin Pitcher and James Riely.
A program verification system for modern software uses a host of technologies, like programming language semantics, formalization of good programming idioms, inference techniques, verification-condition generation, and theorem proving. In this talk, I will survey these techniques from the perspective of the Spec# programming system, of which I will also give a demo. I will reflect on some lessons learned from building automatic program verifiers, as well as highlight a number of remaining challenges.