M. Calder and A. Miller.
Using
SPIN for
Feature Interaction: Analysis -- a Case Study.
Proceedings of the 8th International SPIN Workshop (SPIN 2001),
Toronto, Canada,
Lecture Notes in Computer Science, Volume 2057, pp. 143--162, 2001.
M. Calder and A. Miller.
Using the Model Checker SPIN to Detect Feature Interactions in
Telecommunications Services.
Submitted for publication.
Also University of Glasgow, Computing Science Technical Report
TR-2001-91. 2001.
M. Calder and A. Miller.
Using
SPIN to Analyse the FireWire Protocol -- a Case Study.
To appear in Special Issue of FACS (Formal Aspects of
Computing Science) 2001.
- M. Calder, S. Maharaj, and C. Shankland.
A Modal
Logic for Full LOTOS based on Symbolic Transition Systems.
To appear in The Computer Journal, 2001.
- M. Calder, S. Maharaj, and C. Shankland.
An Adequate
Logic for Full LOTOS.
Proceedings of FME 2001, Lecture Notes in
Computer Science. vol. 2021, pp.384-395, 2001.
- M. Calder and C. Shankland.
A Symbolic Semantics and Bisimulation for Full LOTOS.
Proceedings of FORTE 2001, 21st International
Conference on Formal Techniques for Networked and Distributed Systems, Korea, 2001.
M.~Kim, B.~Chin and S.~Kang and D.~Lee, Eds., pp. 184--200",
Kluwer Academic Publishers, 2001.
- M Calder, E. Magill, S. Reiff-Marganiec, and V. Thayananthan.
Theory and Practice of Enhancing a Legacy Software System.
To appear in Systems Engineering for Business Process Change (volume 2),
P.Henderson (ed.) Springer-Verlag, 2001.
- M. Calder and S. Reiff.
Modelling
Legacy Telecommunications Switching Systems for Interaction Analysis.
Systems Engineering for
Business Process Change, P. Henderson (ed.), pp. 182-195, Springer-Verlag,
2000.
- M. Calder and E. Magill, Editors.
Feature Interactions in Telecommunications and Software Systems VI.
IOS Press, 2000.
- M. Calder, E. Magill and D. Marples.
A Hybrid
Approach to Software Interworking Problems: Managing Interactions between
Legacy and Evolving Telecommunications Software.
IEE
Proceedings - Software, Vol. 146, No. 3, June 1999.
Abstract only
in electronic form, please contact the authors for a hard copy of the full
paper.
- M. Calder and C. Shankland.
A Symbolic
Semantics and Bisimulation for Full LOTOS.
University of Glasgow, Computing Science Technical Report TR-2001-77.
- M. Calder.
What Use are
Formal Analysis and Design Methods to Telecommunications Services?
In
Feature Interactions in Telecommunications and Software Systems, pp.
23-31, IOS Press, 1998.
- M. Thomas.
Modelling and Analysing User Views of Telecommunications Services.
In Feature Interactions in Telecommunications Systems,
pp. 168-183, IOS Press, 1997.
- P. Jeffcutt and M. Thomas.
Organisation, Information and Computation.
ORGANIZATION,
5/3, pp. 397-423, August 1998.
- M. Calder and A. Miller.
Analysing a Basic Call Protocol using PROMELA/XSPIN.
Proceedings SPIN '98: Workshop on Automata Theoretic
Verification with the SPIN model Checker, pp. 169-181, Paris,
G. Holzmann, Ed., 1998.
- C. Shankland and M. Thomas.
Symbolic Bisimulations for Full LOTOS.
In Lecture Notes in
Computer Science vol. 1349, pp. 479-493, Springer-Verlag, 1997.
- S. Aitken, P. Gray, T. Melham, and M. Thomas.
A Study of User
Activity in Interactive Theorem Proving.
Journal of Symbolic
Computation, vol. 25, no. 2, pp. 263-284, February 1998.
Formal Methods and their
Role in Developing Safe Systems.
High Integrity Systems
Journal, Volume 1, Number 5, Oxford University Press, pp. 447-451,
1996.
- C. Kirkwood and M. Thomas.
Experiences with LOTOS:
A Report on Two Case Studies.
Proceedings of WIFT '95
159-172, pp. IEEE Computer Society Press, 1995.
- M. Thomas and B. Ormsby.
On the Design
of Side-Stick Controllers in Fly-By-Wire Aircraft.
ACM Applied
Computing Review , Volume 2, Number 1, Spring 1994.
(Sometimes the picture causes ghostview problems; a version of the paper
without the graphic is here.)
- U. Martin and M. Thomas.
Verification
Techniques for LOTOS.
Proceedings of Formal Methods Europe '94,
Lecture Notes in Computer Science, Volume 873, Springer Verlag,
1994.
- M. Thomas.
The Story of the
Therac-25 in LOTOS.
High Integrity Systems Journal, Volume 1,
Number 1, Oxford University Press, pp. 3-17, 1994.
- M. Thomas.
A Proof of Incorrectness
using LP: the Editing Problem from the Therac-25.
High Integrity
Systems Journal, Volume 1, Number 1, Oxford University Press, pp.
35-49, 1994.
- P. Jeffcutt and M. Thomas.
Order, Disorder and the Unmanageability of
Boundaries in Organised Life.
In the Realm of Organisation,
R. Chia (ed.), Routledge, 1997.
- M. Thomas and P. Watson.
Solving Divergence in
Knuth-Bendix Completion by Enriching Signatures.
Theoretical Computer
Science (Elsevier) 112 pp. 145 - 185, 1993.
- M. Thomas.
A Translator Tool for ASN.1 into LOTOS.
Formal
Description Techniques V. Elsevier (North Holland) Science Publishers,
M. Diaz, R. Groz (eds.), B.V. Amsterdam, 1993, pp. 37-52, 1993.
- M. Thomas.
Algebraic Semantics.Chapter 4
in D.A. Watt,
Programming Language Syntax and Semantics
pp. 147-183, Prentice Hall 1991.
- M. Thomas and P. Watson.
Generalising Sequences of Rewrite Rules by
Synthesising New Sorts.
Extended Abstract, Functional Programming,
Glasgow 1990, pp.268-273, Workshops in Computing, S.
Peyton-Jones, G. Hutton, C. Kehler Holst (eds.), Springer-Verlag 1991.
- M. Thomas.
From 1 Notation to Another One: An ACT-ONE Semantics for
ASN.1.
Formal Description Techniques II , pp. 517-532, S.T.
Vuong (Ed.), Elsevier (North Holland) Science Publishers, B.V. Amsterdam, 1990.
- M. Thomas and K. Jantke.
Inductive Inference for Solving Divergence
in Knuth-Bendix Completion.
Proceedings of Analogical and Inductive
Inference '89, Lecture Notes in Computer Science no. 397, pp.
288-303,Springer-Verlag, 1989.
- M. Thomas.
Implementing
Algebraically Specified Abstract Data Types in an Imperative Programming
Language.
Proceedings of TAPSOFT, Pisa, March 1987, Lecture Notes
in Computer Scienceno. 250, pp. 197-211, Springer-Verlag, 1987.
- Verification of LOTOS Specifications, Final Project Report, from SERC/IED
Project IEATP/SE/IED4/1/1477. March 1993.
Published as University of
Glasgow Department of Computing Science Research Report FM-1993-8.
Prof. Muffy Calder,
Department of Computing Science,University of Glasgow,
Glasgow, Scotland, G12 8QQ.
Telephone +44 141 330 4969, Fax +44 141 330 4913.
Email muffy@dcs.glasgow.ac.uk