iqps.bib
@PHDTHESIS{Moo06,
AUTHOR = {Mooij, Arjan J.},
TITLE = {Constructive formal methods and protocol standardization},
SCHOOL = {Technische Universiteit Eindhoven},
YEAR = 2006,
MONTH = OCT,
PDF = {http://alexandria.tue.nl/extra2/200611509.pdf}
}
@TECHREPORT{DM06b,
AUTHOR = {Dongol, Brijesh and Mooij, Arjan J.},
TITLE = {Streamlining progress-based derivations of concurrent programs},
INSTITUTION = {School of Information Technology and Electrical Engineering, The University of Queensland},
YEAR = 2006,
TYPE = {Technical Report},
NUMBER = {SSE-2006-06},
ABSTRACT = {The logic of Owicki and Gries is a well known logic for verifying
safety properties of concurrent programs. Using this logic, Feijen and
van Gasteren describe a method for deriving concurrent programs based
on safety. In this work, we explore derivation techniques of
concurrent programs using progress-based reasoning. We use a framework
that combines the safety logic of Owicki and Gries, and the progress
logic of UNITY. Our contributions improve the applicability of our
earlier techniques by reducing the calculational overhead in the
formal proofs and derivations. To demonstrate the effectiveness of our
techniques, a derivation of Dekker's mutual exclusion algorithm is
presented. This derivation leads to the discovery of some new and
simpler variations of this famous algorithm.
},
PDF = {pub/Dongol-Mooij-2006.pdf}
}
@INPROCEEDINGS{MRW06,
AUTHOR = {Mooij, Arjan J. and Romijn, Judi M.T. and Wesselink, Wieger},
TITLE = {Realizability criteria for compositional MSC},
BOOKTITLE = {Proceedings of the 11th international conference on Algebraic Methodology And Software Technology (AMAST 2006)},
YEAR = 2006,
EDITOR = {Johnson, M. and Vene, V.},
VOLUME = 4019,
SERIES = {LNCS},
PAGES = {248--262},
PUBLISHER = {Springer-Verlag},
NOTE = {An earlier extended version appeared as Computer Science Report 06-11, Technische Universiteit Eindhoven, March 2006.},
ABSTRACT = {Synthesizing a proper implementation for a scenario-based specification is often
impossible, due to the distributed nature of implementations. To be able to
detect problematic specifications, realizability criteria have been identified,
such as non-local choice.
In this work we develop a formal framework to study realizability of
compositional MSC [GMP03]. We use it to derive a complete classification
of criteria that is closely related to the criteria for MSC from [MGR05].
Comparing specifications and implementations is usually complicated, because
different formalisms are used. We treat both of them in terms of a single
formalism. Therefore we extend the partial order semantics of [Pra86,KL98]
with a way to model deadlocks and with a more sophisticated way to address
communication.
},
PDF = {pub/AMAST06-Mooij-Romijn-Wesselink.pdf}
}
@INPROCEEDINGS{DM06,
AUTHOR = {Dongol, Brijesh and Mooij, Arjan J.},
TITLE = {Progress in deriving concurrent programs: emphasizing the role of stable guards},
BOOKTITLE = {Proceedings of the 8th international conference on Mathematics of Program Construction (MPC 2006)},
YEAR = 2006,
EDITOR = {Uustalu, T.},
VOLUME = 4014,
PAGES = {140--161},
SERIES = {LNCS},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {We present some techniques to obtain smooth derivations of concurrent
programs that address both safety and progress in a formal manner.
Our techniques form an extension to the calculational method of
Feijen and van Gasteren using a UNITY style progress logic. We
stress the role of stable guards, and we illustrate the derivation
techniques on some examples in which progress plays an essential
role.
},
PDF = {pub/MPC06-Dongol-Mooij.pdf}
}
@PROCEEDINGS{RSP2005,
TITLE = {Integrated Formal Methods : 5th International
Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005.},
BOOKTITLE = {Integrated Formal Methods : 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005.},
EDITOR = {Judi Romijn and Graeme Smith and Jaco van de Pol},
SERIES = LNCS,
VOLUME = 3771,
PUBLISHER = {Springer-Verlag},
YEAR = 2005
}
@INPROCEEDINGS{MW05,
AUTHOR = {Mooij, Arjan J. and Wesselink, Wieger},
TITLE = {Incremental verification of {Owicki/Gries} proof outlines using {PVS}},
BOOKTITLE = {Proceedings of the 7th International Conference on Formal Engineering Methods (ICFEM 2005)},
YEAR = 2005,
EDITOR = {Lau, Kung-Kiu and Banach, Richard},
VOLUME = 3785,
SERIES = {LNCS},
PAGES = {390--404},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {Verifications of parallel programs are frequently based on
automated state-space exploration techniques known as model
checking. To avoid state-space explosion problems, theorem proving
techniques can be used, for example by manually annotating
programs with suitable assertions and using these assertions to
prove their correctness (e.g. using the Owicki-Gries theory). We propose
a method to support assertion-based methods with theorem provers
like PVS. Emphasis is on the typical incremental character of
assertion-based methods, and on automated strategies for proving
correctness of the proof outlines.},
PDF = {pub/MW2005.pdf}
}
@INPROCEEDINGS{WGMS05,
AUTHOR = {Wesselink, Wieger and Goga, Nicolae and Mooij, Arjan J. and Spronk, Rene},
TITLE = {Formal methods impact on {ANSI} standard {HL7/IM}: filling gaps in {MSC} theory},
BOOKTITLE = {Proceedings of the 18th Canadian Conference on Electrical and Computer Engineering (CCECE 2005)},
YEAR = 2005,
PAGES = {1656-1659},
PUBLISHER = {IEEE},
ABSTRACT = {Health Level Seven (HL7) is an ANSI standard that provides a
comprehensive framework for electronic health information. The
most-widely used HL7 specification is called Infrastructure
Management, which facilitates health-care applications to exchange
key sets of clinical and administrative data. This paper results
from a cooperation between the authors of the HL7 standard and
academics who have actively participated in an HL7 technical
committee. The challenge taken is to apply formal methods to a
standard in creation, which can be incomplete and subject to
change. Based on this contribution to HL7, we address some gaps in
the current theory on Message Sequence Chart with respect to
deferred behavior and to non-local choice.},
PDF = {pub/WGMS2005.pdf}
}
@INPROCEEDINGS{MGR05,
AUTHOR = {Mooij, Arjan J. and Goga, N. and Romijn, Judi M.T.},
TITLE = {Non-local Choice and Beyond: Intricacies of MSC Choice Nodes},
BOOKTITLE = {Fundamental Approaches to Software Engineering: 8th International Conference, FASE 2005},
YEAR = 2005,
EDITOR = {Cerioli, Maura},
VOLUME = 3442,
SERIES = {LNCS},
PAGES = {273-288},
ABSTRACT = {MSC is a visual formalism for specifying the behavior of systems. To obtain
implementations for individual processes, the MSC choice construction poses
fundamental problems. The best-studied cause is non-local choice, which e.g.
is unavoidable in systems with autonomous processes. In this paper we
characterize two additional problematic classes of choice nodes. Based on these
three classes we point out some errors in related work. Extending our work on
pragmatic implementations of non-local choice, we motivate a different choice
semantics which allows a little more behavior. Finally, inspired by practical
case studies, we present the first implementation approach for non-local choice
nodes that can handle arbitrary numbers of processes.},
PDF = {pub/MGR05.pdf}
}
@INPROCEEDINGS{MG2004,
AUTHOR = {Mooij, A. J. and Goga, N.},
TITLE = {Dealing with Non-local Choice in {IEEE} 1073.2's Standard for Remote Control},
BOOKTITLE = {System Analysis and Modeling: 4th International {SDL} and {MSC} Workshop, SAM 2004},
YEAR = 2005,
EDITOR = {Amyot, Daniel and Williams, Alan W.},
VOLUME = 3319,
SERIES = {LNCS},
PAGES = {257-270},
ABSTRACT = {Currently, communication protocols for medical devices are being
developed for the IEEE 1073.2 standard. The protocol description
in its draft remote control package consists of a collection of
intended behaviors in terms of MSCs. We have contributed to
actually constructing the protocol, ranging from determining an
hMSC for these MSCs, via synthesizing process implementations, to
integrating it with the basic underlying IEEE 1073.2 protocol.
In this paper we report on the non-local choice problems we
encountered. We present a practical solution (i.e. an
implementation) which on the one hand is close to the behavior
specified in the hMSC, and on the other hand meets correctness
properties such as deadlock freedom. These properties have been
checked using the Spin model checker. We also give some directions
for generalizing and extending this work.},
PDF = {pub/SAM-Mooij-Goga2004.pdf}
}
@INPROCEEDINGS{GR2004,
AUTHOR = {Goga, N. and Romijn, J.M.T.},
TITLE = {Guiding {Spin} Simulation},
BOOKTITLE = {/Proceedings of ICFEM'2004/},
EDITOR = {J. Davies and M. Barnett and W. Schulte},
VOLUME = 3319,
SERIES = {LNCS},
PAGES = {257-270},
ABSTRACT = {In this paper we present a technique for the Spin tool,
inspired by practical experiences with Spin and a FireWire protocol. We
show how to guide simulations with Spin, by constructing a special guide
process that limits the behaviour of the original system. We set up a
theoretical framework in which we prove under some sufficient conditions
that the adjusted system (with the added guide process) exhibits a subset
of the behaviour of the original system, and has no new deadlocks.
We have applied this technique to a Promela specification of the IEEE
1394.1 FireWire net update algorithm. The experiment shows that this
technique increases the error detecting power of Spin in the sense that
we found errors in the guided specification, which could not be
discovered with Spin simulation and validation in the original
specification.},
PS = {pub/GR2004.ps.gz},
PDF = {pub/GR2004.pdf}
}
@INPROCEEDINGS{MGW2004,
AUTHOR = {Mooij, Arjan J. and Goga, Nicolae and Wesselink, Wieger},
TITLE = {A Distributed Spanning Tree Algorithm for Topology-Aware Networks},
BOOKTITLE = {Design, Analysis, and Simulation of Distributed systems},
YEAR = 2004,
EDITOR = {Unger, Herwig},
PAGES = {169--178},
PUBLISHER = {The Society for Modeling and Simulation International},
ABSTRACT = {A topology-aware network is a dynamic network in which the nodes
can detect whether locally topology changes occur. Many modern
networks, like IEEE 1394.1, are topology-aware networks. We
present a distributed algorithm for computing and maintaining an
arbitrary spanning tree in such a topology-aware network. Although
usually minimal spanning trees are studied, in practice arbitrary
spanning trees are often sufficient. Since our algorithm is not
involved in the detection of topology changes, it performs better
than the spanning tree algorithms in standards like IEEE 802.1.
Because reasoning about distributed algorithms is rather tricky,
we use a systematic approach to prove our algorithm.},
PDF = {pub/DASD-Mooij-Goga-Wesselink2004.pdf}
}
@ARTICLE{Rom2004a,
AUTHOR = {J.M.T. Romijn},
TITLE = {Improving the Quality of Protocol Standards:
Correcting {IEEE} 1394.1 FireWire Net Update},
JOURNAL = {Nieuwsbrief van de Nederlandse Vereniging voor
Theoretische Informatici},
VOLUME = 8,
PAGES = {23--30},
YEAR = 2004,
ABSTRACT = {The new IEEE 1394.1 FireWire draft standard, which is
expected to be finalised this year, contains a new protocol for
constructing and maintaining spanning trees in the network topology,
called net update. This protocol is complex and merits formal
specification and analysis. In the scope of the NWO Vernieuwingsimpuls
Project `Improving the Quality of Protocol Standards', we have taken
part in the standardisation process, and have helped the development of
this protocol through Promela prototyping (Spin simulation and model
checking), PVS protocol derivation and manual proof. Our efforts have
resulted in the discovery and correction of many errors, omissions and
inconsistencies, as well as the addition of the correctness properties
of the protocol to the standard description.},
PS = {pub/ROM2004.ps.gz},
PDF = {pub/ROM2004.pdf}
}
@TECHREPORT{MGW2003,
AUTHOR = {Mooij, Arjan J. and Goga, Nicolae and Wesselink, Wieger},
TITLE = {A Distributed Spanning Tree Algorithm for Topology-Aware Networks},
INSTITUTION = {Technische Universiteit Eindhoven},
YEAR = {2003},
TYPE = {Computer Science Report},
ADDRESS = {Eindhoven},
MONTH = {jul},
ABSTRACT = {A topology-aware network is a dynamic network in which the nodes
can detect whether locally topology changes occur. Many modern
networks, like IEEE 1394.1, are topology-aware networks. We
present a distributed algorithm for computing and maintaining an
arbitrary spanning tree in such a topology-aware network. Although
usually minimal spanning trees are studied, in practice arbitrary
spanning trees are often sufficient. Since our algorithm is not
involved in the detection of topology changes, it performs better
than the spanning tree algorithms in standards like IEEE 802.1.
Because reasoning about distributed algorithms is rather tricky,
we use a systematic approach to prove our algorithm.},
PS = {pub/MGW2003.ps.gz},
PDF = {pub/MGW2003.pdf}
}
@INPROCEEDINGS{MGWB2003,
AUTHOR = {Arjan J. Mooij, Nicolae Goga, Wieger Wesselink and Dragan Bosnacki},
TITLE = {An Analysis of Medical Device Communication Standard IEEE 1073.2},
YEAR = {2003},
BOOKTITLE = {Proceedings of the Second IASTED International Conference on Communication Systems and Networks},
PUBLISHER = {ACTA Press},
ABSTRACT = {We analyze
pre-standard ENV 13735 of the upcoming IEEE 1073.2 standard, which
standardizes some communication protocols between dynamically
interconnected medical devices. The latter standard is currently
under development, which gives us an opportunity to influence its
final contents using our results. The approach we use is to make
formal models of the protocols, and to analyze them using the
model-checking tool Spin. Our analysis revealed several omissions,
inconsistencies and other types of errors in the protocols and
their descriptions. We discuss possible sources of
these problems, and propose some fixes.},
PS = {pub/MGWB2003.ps.gz},
PDF = {pub/MGWB2003.pdf}
}
@TECHREPORT{MW2003,
AUTHOR = {Mooij, Arjan J. and Wesselink, Wieger},
TITLE = {A Formal Analysis of a Dynamic Distributed Spanning Tree Algorithm},
INSTITUTION = {Technische Universiteit Eindhoven},
YEAR = {2003},
TYPE = {Computer Science Report},
ADDRESS = {Eindhoven},
MONTH = {dec},
ABSTRACT = {We analyze the spanning tree algorithm in the IEEE 1394.1 draft
standard, which correctness has not previously been proved. This
algorithm is a fully-dynamic distributed graph algorithm, which,
in general, is hard to develop. The approach we use is to formally
develop an algorithm that is almost equivalent to it: First, based
on a formal specification and an abstraction of the network, we
systematically construct an algorithm including its correctness
proof. Afterwards we implement this algorithm in terms of IEEE
1394 devices under maintenance of its correctness.},
PS = {pub/MW2003.ps.gz},
PDF = {pub/MW2003.pdf}
}
@INPROCEEDINGS{LRG2003,
AUTHOR = {Langevelde, I.A. van and Romijn, J.M.T. and Goga, N.},
TITLE = {Founding FireWire Bridges through Promela Prototyping},
BOOKTITLE = {Proceedings of 17th International Parallel and
Distributed Processing Symposium (IPDPS), 8th International Workshop on
Formal Methods for Parallel Programming: Theory and Applications (FMPPTA)},
PUBLISHER = {IEEE Computer Society Press},
YEAR = 2003,
ABSTRACT = {The standardisation procedure of the IEEE P1394.1 Draft Standard for High
Performance Serial Bus Bridges is supported through the use of the
state-of-the-art model checker Spin, which has been used to simulate the
complex net update procedure of the standard, and the use of which will
eventually be refined to obtain a solid model checking analysis of the
standard. A concise description of net updates is formalised in terms of
spanning trees, and it is shown how Spin was used to track down errors in the
standard and to gather support for the solutions proposed.},
PS = {pub/LRG2003.ps.gz},
PDF = {pub/LRG2003.pdf}
}
This file has been generated by
bibtex2html 1.61