2009-02-16 Matthew Lang lecture

Matthew Lang
Department of Computer Science and Engineering
Ohio State University
Monday, February 16, 2009
OLB classroom 105, 4pm

Maximal Software

Maximality is a property of software; just as we call software “correct,” “fast,” or “elegant,” we can call software “maximal.” Typically, when we design and reason about software, we are concerned with whether or not the software is correct–that it only does what is permitted by its specification. Maximality is a stronger property than correctness; maximal software is not only correct, but is capable of doing everything permitted by its specification. That is, maximal programs do not restrict the non-determinisim that their specifications provide. Though this property sounds exotic, it's something that–in many cases–we intuitively desire of our software. In this talk, we'll formalize this intuitive desire by defining maximality, discuss some areas where requiring maximality is especially important, and examine (as well as try to build) some examples of maximal software. We will also look at some challenges that we face when designing maximal software and the theoretical results that these challenges stem from. Particularly, we'll see that there are specifications for which no maximal implementation exists and that maximality is not compositional (we can't guarantee that a large system is maximal just by showing that it's built from maximal components). We will also discuss some open questions and exciting research opportunities surrounding reasoning about maximality properties.