Embedded and Distributed Systems
Research Group of Prof. Peter Bernard Ladkin, Ph.D.
Research and other projects
Contents- Previous Research Projects
- 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)
Research Projects
-
Causal Analysis of Systems
The project includes WBA and OHA, below. In addition, Jan Sanders is investigating the preparation of a database of causal analyses of incidents, and methods for searching that database according to causal features of interest, using the SERAS suite of causal analysis tools from Causalis Limited.
- WBA: Why-Because Analysis of failures [ Home Page | Demo ]
-
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).
-
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.
-
Safety and Security Issues in Human-Machine Cognitive Interaction
-
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
-
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. -
Foundations of Systems Theory
[ Home Page ]
-
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.
Previous Research Projects
-
Elearn: Internet Support for Teaching
[ The Elearn Machine ]
-
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.
-
Compendia: Development of On-line Compendia
-
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.
-
NBU: Notebook University
[
Subproject Home Page ]
-
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.
-
Y2K: Classification and Analysis of Date Representation
Problems
[ Home Page]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
-
ManGen: Formally Correct and Complete Operating Manuals
[ Publications ]
-
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.
-
MFGfor: Semantics and Simulation of Message Flow Graphs
[ Home Page ]
-
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.
-
TLA: Development and Use of the TLA logic and TLA+
specification language
[ 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.
- RLPver - Verification of the Radio Link Protocol (RLP1)
[ Home Page ]
-
ConSat/TemLog: Constraint Satisfaction and Temporal Reasoning
[ Publications ]
-
Ladkin writes occasional papers in constraint satisfaction and
also in temporal reasoning and logic (besides TLA). These papers
are collected on his abstracts page.