Today’s development of modern software-based Systems is characterised by (1) vaguely defined problems (the result of some requirements engineering), (2) typically expressed in natural language or, in the best case in a semi-formal notation, should be (3) implemented on top of large software libraries or other third party code as an overall system of millions of lines of code to (4) run on a highly complex enterprise environment, which may even critically involve services connected via wide area network, i.e., the Internet, and it should, of course, be (5) easily adaptable to changing requests.
Practice answers these requests with quite some success with approaches like extreme programming and Scrum, which essentially replace any kind of foundational method with close cooperation and communication within the team and with the customer, combined with early prototyping and testing. Main critique to this formal methods-free approach is merely its lack of scalability, which is partly compensated by involving increasingly complex third party components, while keeping the complexity of their orchestration at a Srum-manageable level.
Does this state of the art reduce the role of the classical formal methods-based approaches in the sense of Hoare and Dijkstra to the niche of (extremely) safety-critical systems? Simply because it is unclear
- What should be formally verified in cases where the problem is not stated precisely upfront? In fact, in most software projects, adapting the development to the changing or needs revealed last-minute is the dominating task?
- What does a fully verified program help, if it comes too late? In fact, in many projects the half-life period is far too short to accommodate any verification activities.
In fact, in some sense the opposite is true, namely that the formal methods developed in the last decade are almost everywhere. E.g., type systems are omnipresent, but seamlessly working in the back of most IDE’s, which are typically supported by complex data ﬂow analyses and sophisticated code generation methods. In addition, (software) model checking has become popular to control application-speciﬁc properties, and even the originally very pragmatic software testing community gradually employs more and more model-based technologies.
However, admittedly, development and debugging as supported by complex integrated development environments (IDEs) like Eclipse and Netbeans or by dedicated bugtracking tools do not attempt to guarantee correctness by construction, the ultimate goal of Dijkstra and Hoare. Rather they are characterized by their community-driven reactiveness:
- software is developed quickly by large communities,
- documentation is largely replaced by online forums,
- quality assurance is a community effort,
- success of a software depends on the vitality of its community.
The LNCS Transactions on Foundations for Mastering Change (FoMaC) intend to establish a forum for foundational research that fosters a discipline for rigorously dealing with this phenomenon. In particular it addresses the very nature of today’s agile system development, which is characterised by unclear premises, unforeseen change, and the need for fast reaction, in a context of hard to control frame conditions, like third party components, network-problem, and attacks.
We envision focused contributions that reflect and enhance the state of the art under the perspective of change. This may comprise new theoretical results, analysis technology, tool support, experience reports and case studies, as well as pragmatics for change, i.e. user-centered approaches that make inevitable changes controllable in practice.