Correct Software in Web Applications and Web Services

• Bernhard Thalheim
• Klaus-Dieter Schewe
• Andreas Prinz
• Bruno Buchberger

Web applications have become one of the largest area for the application of software engineering methods. At the beginning web applications were only simple information services, which soon developed into large database-backed web information systems, i.e. data-intensive systems that are accessed and maintained via the world-wide web. More recently, the area of web services has emerged referring to software components on some web server that can be accessed by and integrated into other software systems. There is a tendency to extend web information systems and web services towards large-scale inter-operable systems. This marks a shift towards computation in the public domain using the internet as the medium for interaction of software components.

Despite the immense importance of web applications for software engineering there is a lack of well-founded development methods. Surprisingly, many web applications are created in an ad-hoc manner without use of sophisticated formal methods. Quality assurance is to a large extent ignored. This constitutes a barrier to productive software development; in other words, the envisioned and most likely technically possible shift to computation in the public domain will only become reality, if the resulting systems are trustworthy with respect to consistency, reliability, performance, and security. Thus, there is a need for development methodst hat lead to provably correct web application systems.

On the other hand, over the last decades many sophisticated formalized methods in software engineering have been developed and applied in various areas with many success stories to the date. The Theorema project at the Research Institute for Symbolic Computation (RISC) is a project and a software system that aims at supporting the entire process of mathematical theory exploration: invention of mathematical concepts, invention and verification (proof) of propositions about concepts, invention of problems formulated in terms of concepts, invention and verification of algorithms solving problems, algorithm synthesis, and storage and retrieval of the formulae invented and verified during this process. The Theorema system consists of a general higher-order predicate logic frame and a collection of special provers that call each other depending on the particular proof situations. The individual provers imitate the proof style of human mathematicians and produce human-readable proofs in natural language presented in nested cells. The special provers are intimately connected with the functors that build up the various mathematical domains.

Similarly, abstract state machines (ASMs) provide a general method to combine specifications on any desired level of abstraction, ground modeling (requirements capture) techniques and stepwise refinement to executable code providing the basis for experimental validation and mathematical verification. ASMs have been successfully applied to diverse areas such as specification and verification of the implementation of programming languages (e.g. Prolog2WAM, Occam2 Transputer, Java2JVM, C#2CLR), of chip design, train control systems, the Mondex electronic purse, and many more. These success stories involve verification by mathematical proofs as well as proofs by theorem provers (e.g. KIV, PVS, ISABELLE) or model checking with justifiable effort.

The key problem addressed by the proposed ESF explorative workshop is that there is almost no connection between the research on these industrially successful formal methods in software engineering and the important area of web applications. Researchers in symbolic computation, abstract state machines, automated reasoning, and verification need input from researchers in web information systems, web services, interoperability and service-oriented architectures to tailor their research to the needs of the applications, and researchers in web applications engineering need support to address the challenging correctness problems.