• The Causal Analysis of Systems
  • WBA: Why-Because Analysis
  • OHA: Ontological Hazard Analysis
• Safety and Security Issues in Human-Machine Cognitive Interaction
• Sustainable Protocols
• Foundations of Systems Theory

• Elearning Project
• Compendium Project
• Notebook University
• Y2K: Procedures for classifying and analysing `Year 2000'-type Problems (until 2001)
• ManGen: Formally Correct and Complete Operating Manuals (until 2000)
• MFGfor: Semantics and Simulation of Message Flow Graphs (until 1998)
• TLA: Development and Use of the TLA logic and TLA+ specification (until 1997) language
• ConSat/TemLog: Constraint Satisfaction and Temporal Reasoning (until 1996)

• WBA: Why-Because Analysis of failures [ Home Page | Demo ]
The investigation of failures of complex systems is a wide field of practical interest which has traditionally lacked significant formal methods. We have developed the formal Why-Because Analysis (WBA) method, which enables one to develop, then formally to prove the correctness and relatively sufficiency of causal explanations. This formal technique is based on formal semantics and logic, and separates the various explanatory domains: time, causation, and deontics (regulations, obligations and operating procedures). The primary application domain to date has been transportation accidents. We have concentrated mainly on aircraft accidents; colleagues using WBA at Siemens Transportation Systems and the Technical University of Braunschweig have concentrated on railway accidents.
• OHA: Ontological Hazard Analysis
  Our current work (2009) is centered on derivation of safety requirements by means of the in-house-developed method Ontological Hazard Analysis which uses specific technical methods to identify and keep track of hazards during refinement from requirements specifications down to, in some cases, executable source code. Bernd Sieker has just finished his doctoral thesis (May 2009) on the ontological hazard analysis of train dispatching according to German regulations. The target code is SPARK (annotated ADA executable).

Peter Ladkin is a Principal Investigator in CITEC, the Bielefeld Centre of Excellence in Cognitive Interaction Technology. His project investigates principles for ensuring the safety and security of interactions between humans and machines such as mobile robots, of which there are quite a few around CITEC, and highly automated airplanes. We make available here the Project Description which was accepted by the CITEC Scientific Council in May 2009. Bernd Sieker is the project lead researcher May 2009-October 2012.

Sustainable protocols are methods for completing transactions and interactions that depend upon very weak social assumptions. For example, authentication needs in Western countries suggest the use of digital signatures, which are administered through a certification authority. How does one offer authentication for digital interactions in societies in which trust in central authority is very weak or absent? Avinanta Tarigan from Jakarta finished his thesis, which offered an answer to this question, in 2007.

I Made Wiryana, also from Jakarta, has led many high-profile urgent projects technically. He is a personal IT advisor to the Indonesian president and technical director of the presidential WWW site. Made's doctoral thesis concerned his methods for ensuring quality of the service provided to users by an software-based IT development in an environment in which there are many conflicted cultural constraints. His work involved "Participatory Action Research", that is, he reported in his thesis on actual projects which he had led. He employed "Lightweight Why-Because Analysis", LWBA, an adaptation of WBA to analyse causally the provision of service in an IT project, and thereby to find out where reasons might lie for success or failure. His dissertation was awarded a distinction, one of seven in Informatics in our faculty in the period August 2008 - July 2009.

Aditya Priowirjanto in analysing the implementation of WiMax as a technology of choice for wide-coverage Internet access in Indonesia.

This work investigates the logical and philosophical foundations of the notions of success and failure of complex systems. The first question is: what is a system? Most social theorists, biologists, physicists, organisational theorists, and computer scientists take a system to be a collection of objects with behavior (often called actors. A central task is to derive the emergent behavior of the collection (the system) from knowledge of the behavior and interactions of the actors. Another task is to explain the influence of the system on the behavior and interactions of the actors. Systems interact with their environment, which is the collection of objects that are not considered part of the system. Systems also have subsystems, which are subcollections of actors with distinctive interactions of special interest, or whose emergent subsystem properties are interesting in some way.

We aim to define a standard set of concepts for systems theory which will incorporate the notions of system in such diverse fields as Shannon's communication theory, Luhmann's sociological systems theory, Coleman's Rational Choice social theory, biological systems theory, systems of subatomic particles, and computer operating systems and software systems.

We are particularly concerned with teleological systems, which are systems with a goal, corresponding to one of the binary classifiers in Parsons' social systems taxonomy, and the main interest of artifactual systems engineers. Our main interest is in the correctness and failure of such systems, as exemplified in the WBA and CSA projects.

One of us has developed the internet communications platform Worksphere, which administers internet-based communication for students in elearning courses. WWW-based content for courses for Technical Informatics (hardware architecture and basic operating systems and system administration topics), Computer Networking, and Digital Systems Safety is under development. The Technical Informatics modules are used in required courses for computer science students at the University of Bielefeld, and the networking and systems safety material is under development for advanced courses.

Our aim is to distribute both platform and course work, and to be able to administer locally in Bielefeld courses based in other locations which use the platform.

Worksphere is in use in the RVS group, and in commercial use in a distance learning degree program of the Department of Health Studies at the University of Bielefeld. Further installations are planned in some Information Technology Training Colleges in Indonesia.

Worksphere installations may be commercially designed and maintained by the Bielefeld company Nothbaum GmbH.

We also participate in the m² project led by the University of Weimar, to develop an elearning degree course for New Media Art and Design (Mediengestaltung). Our Technical Informatics modules are part of the content of the M2 degree course.

Since 1995 we have built and maintained a Compendium on Computer-Related Incidents with Commercial Aircraft. The current version of the compendium dates from 2000, and a major update in contents is underway. We are transitioning to a more flexible dynamic content presentation system. Besides the compendium on aircraft accidents, we are also starting compendia on sustainable protocols, on practical network security, and on elearning, using the same content presentation system.

We participate in the Notebook University project along with other faculties in the University of Bielefeld. We have equipped students in two years of our degree course in New Media Technics and Design (Mediengestaltung) with highly capable notebook computers, which they use in ten specially designed courses in their degree program. Wireless networking capability and Internet connection is provided by the Computing Center of the university, with coverage of particular seminar and work rooms in which courses and student work take place. The uptake by students of notebook-computer-supported coursework has been heartening, indeed more than we had anticipated. Our major task now is to build on this good start to integrate use of notebook computers into the degree program permanently, and to expand in-class use of notebook computers into other degree courses we offer.

For centuries, dates have been represented in shorthand in human endeavors. Two decimal digits have often represented the year in writing since the Renaissance. There are about to be failures of complex systems due to date representation discontinuities. On 21 August 1999 at 23:59:47, the GPS time data will `roll over' to zero; GPS systems without protection may think they are back at 5 January 1980 (`week 0'). On 1 Jan 2000, many software and hardware system components will `roll over' to 1.1.1900 (the so-called `millenium bug').

Many people, including some reknowned computer scientists, believe that the collection of Year 2000 problems are scientifically trivial. We believe strongly that this is not the case. There are surprisingly few conditions required for adequate data representation. Each one of these five conditions is violated by some instance of a Year 2000 problem. We describe these conditions, and what happens when they are violated, in the article The Analysis of Data Discontinuities.

We have also collected links to Year 2000 WWW sites by institutions and system vendors, and make available some essays by former Deloitte, Touche Global Year 2000 chief Martyn Thomas, as well as essays by ourselves

In cooperation with Harold Thimbleby of the Interaction Center of University College, London, we analysed operating manuals and their formal weaknesses, and helped design tools such as LogToMan (Thimbleby and Ladkin) for the mathematical specification and analysis of human-machine interaction, and the generation of complete and correct operating manuals, especially for safety-critical systems.

In cooperation with Stefan Leue of the University of Waterloo and Barbara Simons, formerly of IBM, Ladkin defined semantics for and analysing Message Flow Graphs and their instantiation as Message Sequence Charts.

[ The TLA Web Page at Leslie Lamport's Home Page | Publications (RVS) ]

We participated in Leslie Lamport's TLA project, to develop and apply the verification logic TLA and its associated specification language TLA+. Subprojects are RLPver (below) and the student project BioSpec. WBA proofs are based partly on TLA, and use the module structure of TLA+ and the hierarchical proof method of Lamport, with the associated LaTeX style files. Includes the subproject
• RLPver - Verification of the Radio Link Protocol (RLP1) [ Home Page ]
  In cooperation with the Telecommunications Software Group at INRS-Télécommunications in Montréal, we worked on the TLA specification and verification of the Radio Link Protocol (RLP1), the datalink layer protocol for TDMA mobile cellular radio. We specified RLP1 hierarchically and verified the upper levels of the specification, culminating in Dirk Henkel's Diplom Thesis, which consisted of 115pp or so of formal TLA verification. From the level below which we verified the correctness of the protocol, the protocol was validated by Jean-Charles Grégoire of INRS-Télécommunications using model checking.

Ladkin writes occasional papers in constraint satisfaction and also in temporal reasoning and logic (besides TLA). These papers are collected on his abstracts page.