Abstract
This research is part of the NWO project "Improving the Quality of Protocol
Standards". In this project we have cooperated with industrial standardization
committees that are developing protocol standards. Thus we have contributed to
these international standards, and we have generated relevant research questions
in the field of formal methods.
The first part of this thesis is related to the ISO/IEEE 1073.2 standard, which
addresses medical device communication. The protocols in this standard were developed
from a couple of MSC scenarios that describe typical intended behavior.
Upon synthesizing a protocol from such scenarios, interference between these scenarios
may be introduced, which leads to undesired behaviors. This is called the
realizability problem.
To address the realizability problem, we have introduced a formal framework that
is based on partial orders. In this way the problem that causes the interference
can be clearly pointed out. We have provided a complete characterization of
realizability criteria that can be used to determine whether interference problems
are to be expected. Moreover, we have provided a new constructive approach
to solve the undesired interference in practical situations. These techniques have
been used to improve the protocol standard under consideration.
The second part of this thesis is related to the IEEE 1394.12004 standard, which
addresses High Performance Serial Bus Bridges. This is an extension of the IEEE
13941995 standard, also known as FireWire. The development of the distributed
spanning tree algorithm turned out to be a serious problem.
To address this problem, we have first developed and proposed a much simpler
algorithm. We have also studied the algorithm proposed by the developers of
the standard, namely by formally reconstructing a version of it, starting from
the specification. Such a constructive approach to verification and analysis uses
mathematical techniques, or formal methods, to reveal the essential mechanisms
that play a role in the algorithm. We have shown the need for different levels of
abstraction, and we have illustrated that the algorithm is in fact distributed at two
levels. These techniques are usually applied manually, but we have also developed
an approach to automate parts of it using stateoftheart theorem provers.
Original language  English 

Qualification  Doctor of Philosophy 
Awarding Institution 

Supervisors/Advisors 

Award date  2 Oct 2006 
Place of Publication  Eindhoven 
Publisher  
Print ISBNs  9038607946 
DOIs  
Publication status  Published  2006 
Fingerprint Dive into the research topics of 'Constructive formal methods and protocol standardization'. Together they form a unique fingerprint.
Cite this
Mooij, A. J. (2006). Constructive formal methods and protocol standardization. Technische Universiteit Eindhoven. https://doi.org/10.6100/IR612838