Selected Publications
1.
M. Calder. M. Sevegnani
Process algebra for event-driven runtime verification: a case study of wireless
network managment.
Proceedings 9th International Conference on Integrated
Formal Methods, IFM 2012, Pisa, Italy, Lecture Notes in Computer Science, volume 7321, pp 21-23,
2012. The original publication is available at www.springerlink.com.
2.
A. Degasperi, M. Calder.
Multi-Scale Modelling of Biological Systems in Process Algebra with Multi-way
Synchronisation.
Proceedings 9th International CMSB 2011
(International Computational Systems Biology), Paris, France. isbn 978-1-4503-0817-5, 2011.
3. R.
Donaldson, C. Talcott, M.
Knapp, M. Calder.
Understanding Signalling Networks as
Collections of Signal Transduction Pathways
Proceedings of 8th International CMSB (Computational Methods in
Systems Biology), ACM, 2010. http://portal.acm.org/citation.cfm?id=1839764\&picked=prox2010.
4.
M. Calder,
P. Gray, A. Miller and C. Unsworth.
An introduction to Pervasive Interface Automata
Proceedings of 7th
International FACS (Formal Aspects of Component Software). LNCS vol. 6921, pp.71-87, 2011.
5. O. Andrei and M. Calder.A Model and Analysis of the AKAP Scaffold
A
Model and Analysis of the AKAP Scaffold.
CS2Bio2010, ENTCS 268, pages 3-15, Elsevier, 2010
6. M.
Calder, O. Andrei, A. Degasperi and R. Donaldson.
From
species to pathway and tissue as process
Proceedings of 8th International CMSB (Computational Methods in
Systems Biology), ACM, 2010. http://portal.acm.org/citation.cfm?id=1839764\&picked=prox2010.
7.
A. Degasperi, M. Calder.
Process
Algebra with Hooks for Models of Pattern Formation.
CS2Bio2010, ENTCS 268, pages 31-47, Elsevier, 2010
8.
A. Degasperi, M. Calder.
Relating
PDEs in Cylindrical Coordinates and CTMCs with Levels of Concentration.
CS2Bio2010, ENTCS 268, pages 49-59, Elsevier, 2010.
9.
R. Donaldson, M. Calder.
Modelling and and Analysis of Biochemical Signalling
Pathway Crosstalk.
ENTCS 118, pp. 01-15, Proceedings FBTC 2010, to appear, 2010.
10. M.
Calder, J. Hillston.
Process algebra modelling styles for biomolecular
processes.
Transactions on Computational Systems Biology XI, LNBI
5750, pp.1-25, Springer, 2009.
11. M.
Calder, P. Gray and C. Unsworth
Tightly coupled verification of pervasive systems
Proceedings of the Third International Workshop on Formal Methods for Interactive
Systems (FMIS 2009) Electronic Communications of the EASST,
volume X, 2009.
12. M.
Calder, S. Gilmore, J. Hillston and V. Vyshemirsky
Formal methods for biochemical signalling pathways
Formal Methods: State of the Art and New Directions, Springer, 2009.
13. A. Miller and M. Calder.
An automatic abstraction technique for verifying featured, parameterised
systems
Theoretical
Computer Science, 404, pp. 235-255, 2008.
14. F. Ciochetta, A.
Degasperi, J. Hillston, M. Calder.
Some investigations concerning the CTMC and the ODE model derived from
Bio-PEPA
Proceedings of FBTC 2008, ENTCS vol. 17350, Elsevier, 2008.
15. M.
Calder, S. Gilmore (Editors)
Computational Methods for Systems Biology
Theoretical Computer Science, volume 408, Elsevier, 2008.
16. D.
Graham, M. Calder, and A Miller
An Inductive Technique for Parameterised Model Checking of Degenerative
Distributed Randomised Protocols
Proceedings of AVOCS 07 (Automated Verification of Critical Systems), ENTCS
vol. 250, pp.87-103, Elsevier
2009.
17. M.
Calder, S. Gilmore (Editors)
Computational Methods for Systems Biology Lecture Notes in
Bioinformatics, volume 4695, Springer, 2007.
18.
M. Calder, S. Gilmore and J. Hillston
Modelling the influence of RKIP on the ERK signalling pathway using the
stochastic process algebra PEPA
Transactions
on Computational Systems Biology VII, vol. 4230, pp. 1-23, Springer, 2006.
19. A.
Miller, A. Donaldson and M. Calder
Symmetry in temporal logic model checking
Computing
Surveys, ACM ,vol. 38, issue 3,pp. 1-36, 2006.
20. A. Miller,
M. Calder and A. Donaldson
A template-based approach for the generation of abstractable
and reducible models of featured networks
Computer
Networks, vol. 51(2), pp. 439-455, Elsevier, 2007.
21. M.
Calder, A. Duguid, S. Gilmore and J. Hillston.
Stronger computational modelling of signalling pathways using both continuous
and discrete-space methods
Computational
Methods in Systems Biology (CMSB 2006), LNBI vol. 421, pp. 63-78, 2006.
22. M.
Calder, V. Vyshemirsky, D. Gilbert, and R. Orton.
Analysis of Signalling Pathways using Continuous Time Markov Chains
Transactions
on Computational Systems Biology VI, vol. 4220, pp. 44-67, Springer, 2006.
23. M. Calder
and A. Miller
Feature
Interaction Detection by Pairwise Analysis of LTL Properties--a case study
Formal Methods
in System Design, Volume 28(30), pp. 213-261, May 2006.
24. M. Calder
and J. Hillston
What do scaffold proteins really do?
Fifth Workshop
on Process Algebra and Stochastically Timed Activities (PASTA 2006), Imperial
College, 2006.
25. A. Miller and M. Calder.
A generic approach for the automatic verification of featured, parameterised
systems
Proceedings of
Eighth International Conference on Feature Interactions in Telecommunications
and Software Systems (ICFI '05) , pp
217-235, IOS Press, 2005.
26. M.
Calder, S. Gilmore and J. Hillston.
Automatically deriving ODEs from process algebra models of signalling
pathways
Proceedings of
CMSB 2005 (Computational Methods in Systems Biology), pp
204-215, 2005.
27. M.
Calder, V. Vyshemirsky, D. Gilbert and R. Orton.
Analysis of Signalling Pathways using the Prism Model
Checker
Proceedings of CMSB 2005 (Computational Methods in Systems Biology), pp
179-190, 2005.
28. W. Kolch, M. Calder and D. Gilbert.
When kinases meet mathematics: the systems biology of MAPK signalling
FEBS Letters, vol. 579,
pp 1891--1895, 2005.
29. R. Orton, O.
Sturm, V. Vyshemirsky, M. Calder, D. Gilbert and W. Kolch.
Computational Modelling of the Receptor
Tyrosine Kinase Activated MAPK Pathway
Biochemical Journal, vol. 392, pp 249--261, 2005.
30. M.
Calder, S. Gilmore and J. Hillston.
Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra
PEPA
Proceedings of
Bio-CONCUR 2004, Electronic Notes in Theoretical Computer Science, 2004.
31. A.
Donaldson, A. Miller and M. Calder.
Finding symmetry in models of concurrent systems by static channel diagram
analysis
Electronic
Notes in Theoretical Computer Science, vol. 128/6, pp
161-177, Elsevier, 2004.
32.
M Calder and A. Miller.
Verifying parameterised, featured networks by abstraction
Proceedings of the first International Symposium on Leveraging
Applications of Formal Methods (ISOLA'04), pp 227--234.
33.
M Calder and A. Miller.
Detecting
Feature Interactions: how many components do we need?
Objects, Agents
and Features. Lecture Notes in Computing Science, vol. 2975, pp 45-66, 2004.
34. P.Saffrey and M. Calder.
Optimising
Communications Structure for Model Checking Lecture Notes in Computer Science,
Proceedings of
FASE 2004, Lecture Notes in Computer Science, vol. 2984, pp
310-3224, Springer Verlag, 2004.
35.
A.Miller and M
Calder.
An
application of abstraction and induction techniques to degenerating systems of
processes.
Proceedings of
the International Workshop on Model-Checking for Dependable Software Intensive
Systems (MCDSIS '03), IEEE Computer Society Press, 2003.
36.
M Calder, M. Kolberg E.
Magill, D. Marples and S. Reiff-Marganiec.
Hybrid
Solutions to the Feature Interaction Problem
Feature
Interactions in Telecommunications and Software Systems VII, IOS Press. pp.187-205, 2003.
37.
M Calder and A. Miller
Generalising Feature Interactions in Email
Feature
Interactions in Telecommunications and Software Systems VII, IOS Press. pp.
295-217, 2003.
38.
M Calder, E. Magill, M. Kolberg,
and S. Reiff-Marganiec.
Feature
Interaction: A Critical Review and Considered Forecast.
Computer
Networks,
Volume 41/1, pp. 115-141, North-Holland. January 2003.
39.
M. Calder and A. Miller.
Using SPIN to
Analyse the FireWire Protocol -- a Case Study.
Formal Aspects
of Computer Science, vol. 14, no. 3, pp. 247266, Springer Verlag,
2003.
40.
M. Calder and A. Miller.
Automated
verification of any number of concurrent, communicating processes.
Proceedings of
17th IEEE Automated Software Engineering (ASE 2002), pp.
227-230, IEEE, 2002.
41.
M. Calder and A. Miller.
Five
ways to use symmetry and induction in the verification of networks of processes
using model-checking.
Proceedings of
Automated Verification of Critical Systems (AVoCS),2002.
42. M.
Calder, S. Maharaj, and C. Shankland.
A Modal Logic for
Full LOTOS based on Symbolic Transition Systems.
The Computer
Journal, Volume 45, No.1, pp. 55--61, 2002.
43.
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.
44.
M. Calder and A. Miller.
Using
the Model Checker SPIN to Detect Feature Interactions in Telecommunications
Services.
University of
Glasgow, Computing Science Technical Report TR-2001-91. 2001.
45.
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.
46.
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, S.Kang and D.Lee (Eds.), pp. 184--200, Kluwer Academic Publishers,
2001.
47.
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.
48.
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.
49.
M. Calder and E. Magill, Editors.
Feature
Interactions in Telecommunications and Software Systems VI.
IOS Press, 2000.
50.
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.
51.
M. Calder and C. Shankland.
A Symbolic
Semantics and Bisimulation for Full LOTOS.
University of
Glasgow, Computing Science Technical Report TR-2001-77.
52. 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.
53.
M. Thomas.
Modelling and Analysing User
Views of Telecommunications Services.
In Feature
Interactions in Telecommunications Systems, pp. 168-183, IOS Press,
1997.
54.
P. Jeffcutt and M.
Thomas.
Organisation,
Information and Computation.
ORGANIZATION,
5/3, pp. 397-423, August 1998.
55.
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.
56.
C. Shankland and M. Thomas.
Symbolic Bisimulations for Full LOTOS.
In Lecture
Notes in Computer Science vol. 1349, pp. 479-493, Springer-Verlag, 1997.
57.
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.
58. M.
Thomas.
Formal Methods and
their Role in Developing Safe Systems.
High Integrity
Systems Journal, Volume 1, Number 5, Oxford University Press, pp.
447-451, 1996.
59. 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.
60. 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.)
61. 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.
62.
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.
63. 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.
70. M. Thomas and K. Jantke
Inductive
Inference for Knuth Bendix Completion
Lecture Notes
in Computer Science vol. 397 288-303, Springer Verlag, 1989.
73.