PETER GORM LARSEN

GENERAL OVERVIEW

I am working for the Engineering College of Aarhus (IHA) as a professor (in Danish "ingenørdocent") and I am also an adjunct professor at Aarhus University. In parallel with this is have a small one-man consultancy company called PGL Consult where I  assist companies with the use of formal methods (in particular VDM) as well as assist with producing bids, reviewing and writing different kinds of material. The first customers here are Systematic Software Engineering from Denmark and CSK from Japan.

From January 2002 till July 2005 I have worked for Systematic Software Engineering which is a high-tech software development company, where my title was "Chief Business Solution Architect". This means that I was involved with business development with a technical angle where I assisted with the conceptual solution based on an understanding of the customers challenges. I was particularly involved in the defense sector where my main project was the Joint Strike Fighter project.

Previously I was working for IFAD which is a much smaller high-tech IT company since 1989. Here I was head of the department dealing with long-term research for IFAD and consultancy and training services for the VDM technology. As the main VDM consultant I have worked with many large companies including Boeing, British Aerospace, Aerospatiale, Dassault, Matra, Alcatel and Baan. In addition to being a charge of a number of projects at IFAD I am involved with organising the VDM Workshop at the FM'99 symposium. In addition to the publications given below I have been involved in writing a new VDM tutorial book called "Modelling Systems: Practical Tools and Techniques in Software Development". Course material for the book is also available. A new tutorial book for VDM++ has been completed January 2005 together with John Fitzgerald, Paul Mukherjee, Nico Plat and Marcel Verhoef.

At IFAD I have been supervising a number of students (mostly for their final MSc thesis projects) over the years. Subsequently I have been supervising students while working at the Engineering College of Aarhus (from 2005):

• (1992) Marcel Verhoef, (TU Delft, The Netherlands)
• (1993) Kees de Bruin, (TU Delft, The Netherlands)
• (1994) Carsten Anacher (Fachhochschule Wedel, Germany) (BSc)
• (1994) Ivan Overgaard (Odense University, Denmark)
• (1995) Vincent Stephan, (IRESTE, France) (summer student)
• (1995) Brigitte Frölich, (TU Graz, Austria) (PhD)
• (1996) Søren Nielsen, (Odense University, Denmark)
• (1996) Bernhard Aichernig, (TU Graz, Austria)
• (1997) Jesper Kjær Pedersen (Odense University, Denmark)
• (1998) Wendy Schaefer (JPL, USA) (a months visit)
• (1998) Oliver Oppitz, (TU Graz, Austria) (for which a prize was awarded by IEEE)
• (2000) Georg Weissenbacker, (TU Graz, Austria) (summer student)
• (2001) Nicola Trcka, (University of Belgrade, Yugoslavia) (summer student)
• (2005) Jacob Porsborg Nielsen and Jens Kielsgaard Hansen, (Technical University of Denmark, Denmark)
• (2005) Kasper Boe Johansen, (IHA, Denmark)
• (2006) Klaus Pedersen, (IHA, Denmark)
• (2006) Nick Nygaard, (IHA, Denmark)
• (2007) Thomas Christensen (Aarhus University, Denmark)
• (2007) Kasper Høj Jæger Nielsen, (IHA, Denmark)
• (2007) Hugo Macedo (Minho University, Portugal)
• (2007) Sander Vermolen (University of Nijmegen, The Netherlands)
• (2007) Jasper Moltke Nygaard (IHA, Denmark)
• (2007) Rasmus Ask Sørensen (IHA, Denmark)
• (2008) Adriana Sucena (Minho University, Portugal)
• (2008) Carlos Vilhena (Minho University, Portugal)
• (2008) Augusto Ribeiro (Minho University, Portugal)
• (2008) Sune Wolff (IHA, Denmark)
• (2008) Kenneth Lausdahl (IHA, Denmark)
• (2008) Hans Kristian Lintrup (IHA, Denmark)
• (2009) Christian Thillermann (IHA, Denmark)
• (2009) David Holst Møller (IHA, Denmark)
• (2009) Lasse Lorentzen (IHA, Denmark)

PUBLICATIONS

1. VDM-SL Standard

• "The Dynamic Semantics of the BSI/VDM Specification Language." P.G. Larsen and M.M. Arentoft, MSc Thesis, Department of Computer Science, Technical University of Denmark, 1988, 352 pages. (bib entry)

• "Towards a Formal Semantics of the BSI/VDM Specification Language'' P.G.Larsen, M.M.Arentoft, B.Q.Monahan, S.Bear. Published by INFORMATION PROCESSING 89 (IFIP), G.X. Ritter (ed.), Elsevier (North Holland), 1989, August 28-September 1, San Francisco, U.S.A. pp. 95-100 (bib entry)

• "An Overview of the ISO/VDM-SL Standard'' N.Plat, P.G.Larsen. Published by SIGPLAN Notices, Volume 27, Number 8, August 1992 (bib entry)

• "Standards for Non-Executable Specification Languages'' P.G.Larsen, N.Plat. Published by BCS Computer Journal, Volume 35, Number 6, December 1992 (bib entry)

• "Første VDM-SL Standard på vej ''P.G.Larsen. (In Danish) Published by IT Standardnyt, Volume 4, Number 2, Marts 1993 (bib entry)

• "The formal Semantics of ISO VDM-SL'' Peter G. Larsen, Wieslaw Pawlowski. Published in "Computer Standards and Interfaces'' journal, vol. 17, no. 5-6, September 1995 (bib entry).

2. CEDER

• ''A Formal Event Structuring Approach to Real-Time Design'' P.G.Larsen. Published by EUROMICRO '90 Workshop on Real Time, Elektronikcentralen, Hørsholm, Denmark, June 1990, IEEE Computer Society Press (bib entry)

• "An Event Structuring Approach to Real-Time Design'' P.G.Larsen. Published by 2nd Nordic Workshop on Program Correctness, Aalborg, Denmark, October 1990, The University of Aalborg IR 90-05 (bib entry)

3. Tool Supported VDM-SL and VDM++

• "An Executable Subset of Meta-IV with Loose Specification'' P.G.Larsen, P.B.Lassen. Published by VDM '91-Formal Software Development Methods, Springer-Verlag, Noordwijkerhout, The Netherlands, October 1991 (bib entry)

• "Making Specifications Executable - Using IPTES Meta-IV'' M.Andersen, R.Elmstrøm, P.B.Lassen, P.G.Larsen. Published by Microprocessing and Microprogramming, September 1992, Vol. 35, Nos. 1-5 (bib entry)
• Response to "The Formal Specification of Safety Requirements for Storing Explosives'' P.G.Larsen. Published by Formal Aspects of Computing, Vol. 6, No. 5, pp. 565-568, 1994 (bib entry)

• "The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications'' R.Elmstrøm, P.G.Larsen, P.B.Lassen. Published by ACM Sigplan Notices, summer 1994 (bib entry)

• "Combining VDM-SL Specifications with C++ Code." B. Fröhlich and P.G. Larsen. Published in "FME'96: Industrial Benefit and Advances in Formal Methods", Springer-Verlag, March 1996 (bib entry).

• "Modeling and Validating SAFER in VDM-SL" S.Agerholm and P.G.Larsen. Published in Proceedings of the Fourth NASA Langley Formal Methods Workshop, NASA Conference Publication 3356, September 1997 (bib entry).

• "A Proof Obligation Generator for VDM-SL" B.K.Aichernig and P.G.Larsen. Published in FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, Springer-Verlag, LNCS 1125, 1997 (bib entry).

• "A Lightweight Approach to Formal Methods" S.Agerholm and P.G. Larsen. In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998 (bib entry).

• "The Return of VDM to Austria" P.G. Larsen. Published in Telematik (Graz, Austria), 1998 (bib entry).
• Modelling Systems - Practical Tools and Techniques in Software Development, John Fitzgerald and Peter Gorm Larsen, Cambridge University Press, ISBN 0-521-62348-0, 1998 (bib entry).
• Applications of VDM in Banknote Processing, Paul R. Smith and Peter Gorm Larsen, VDM in Practice, September 1999, Toulouse, France (bib entry).

• Using VDMTools to Model and Validate the Cash Dispenser Example, Peter Gorm Larsen, Paul Mukherjee and Kim Sunesen, , Formal Aspects of Computing, 2000, 12:216-217 (bib entry).

• Exploring Timing Properties using VDM++ on an Industrial Application, Paul Mukherjee, Fabien Bousquet, Jerome Delabre, Stephen Paynter and Peter Gorm Larsen, , In Juan Bicarregui and John Fitzgerald, editors, The Second VDM Workshop, 2000 (bib entry).

• Ten Years of Historical Development - Bootstrapping VDMTools, Peter Gorm Larsen, Journal of Universal Computer Science, vol. 7, no. 8, pp. 692-709, 2001 (bib entry).

• "Validated Designs for Object-oriented Systems J.S. Fitzgerald, P.G. Larsen, P. Mukherjee, N. Plat and M. Verhoef, Springer, ISBN 1-85233-881-4, January 2005 (bib entry).
• "Modeling and Validating Distributed Embedded Real-Time Systems with VDM++ M. Verhoef, P.G. Larsen and J. Hooman, Springer Verlag Berlin, in FM 2006: Formal Methods, ISBN 3-540-37215-6, August 2006 (bib entry).
• Interpreting Distributed System Architectures using VDM++ - A Case Study,  Conference of System Engineering Research (CSER), March, 2007 (bib entry).
• Balancing Insight and Effort: the Industrial Uptake of Formal Methods, John Fitzgerald and Peter Gorm Larsen, Formal Methods and Hybrid Real-Time Systems, Essays in Honour of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Springer, LNCS 4700, Macau, pp.237-254, September 2007 (bib entry).
• Validation Support for Distributed Real-Time Embedded Systems in VDM++, John Fitzgerald. Peter Gorm Larsen, Simon Tjell and Marcel Verhoef, High Assurance System Engineering, IEEE, November 2007 (bib entry).
• VDMTools: advances in support for formal modeling in VDM, John Fitzgerald, Peter Gorm Larsen and Shin Sahara, Sigplan Notices, February 2008, pp 3-1 (bib entry).
• Recent Industrial Applications of VDM in Japan, Peter Gorm Larsen and John Fitzgerald, BCS Formal Aspects of Computing, Christmas workshop, December 2007, published May 2008, http://www.bcs.org/server.php?show=nav.10006, eWIC (bib entry).
• Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM, Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald, FM 2008: Formal Methods, LNCS 5014, Eds.: Jorge Cuellar, Tom Maibaum and Kaisa Sere, May 2008 (bib entry).
• Modelling Systems - Practical Tools and Techniques in Software Development, 2nd edition, John Fitzgerald and Peter Gorm Larsen, Cambridge University Press, ISBN 0-521-62348-0, 2009 (bib entry).
• Methods for the Developing Distributed Real-Time Systems using VDM, Peter Gorm Larsen, John Fitzgerald and Sune Wolff, International Journal of Software and Informatics, October 2009 (bib entry).
• Connecting UML and VDM++ with Open Tool Support, Kenneth Lausdahl and Hans Kristian Agerlund Lintrup and Peter Gorm Larsen, Formal Methods 09, November 2009 (bib entry).
• The Overture Initiative - Integrating Tools for VDM, Peter Gorm Larsen, Nick Battle, Miguel Ferreira, John Fitzgerald, Kenneth Lausdahl and Marcel Verhoef, ACM Software Engineering Notes, January 2010, Vol 35 (1) (bib entry)
• Sander Vermolen, Jozef Hooman, and Peter Gorm Larsen, Automating Consistency Proofs of VDM++ Models using HOL, ACM Proceedings of the 25th Symposium On Applied Computing (SAC 2010), 22 - 26 March  2010 (bib entry)

4. SA and VDM

• "Towards an Integrated Combination of SA and VDM'' P.G.Larsen, J.van Katwijk, N.Plat, K.Pronk, H.Toetenel. Published by Workshop "Structured Analysis and Formal Methods'', York, June 1991 (bib entry)

• "A Formal Semantics of Data Flows Diagrams'' P.G.Larsen, N.Plat, H.Toetenel, Formal Aspects of Computing'' 1994, Vol 6, December (bib entry).

• "SVDM: An Integrated Combination of SA and VDM'' P.G.Larsen, N.Plat, K.Pronk, H.Toetenel. Methods Integration Conference, September 1991, Leeds (bib entry).

• "Formal Transformations: Using SA and VDM as Different Views in Software Development''N.Plat, P.G.Larsen, H.Toetenel. Technical Report, which was never properly published

5. PhD Work

• "Towards Proof Rules for the Full Standard VDM Specification Language'' Peter Gorm Larsen. PhD dissertation. Published by DTU, ID-TR: 1995-160, ISSN 0902-2821, Lyngby, Denmark, March 1995 (bib entry).

• "Towards Proof Rules for Looseness in Explicit Definitions from VDM-SL'' P.G.Larsen. Published by International Workshop on Semantics of Specification Languages (SoSL), 25-27 October 1993, Utrecht, Springer 1994 (bib entry)

• "Evaluation of Underdetermined Explicit Definitions'' P.G.Larsen. Published at Formal Methods Europe'94: Industrial Benefit of Formal Methods Barcelona, October 1994 (bib entry)

• "Semantics of Underdetermined Expressions'' Peter G. Larsen, Bo S. Hansen. Technical University of Denmark, Lyngby, ID-TR:1994-151. Extended version. Published by "Formal Aspects of Computing'', January 1996 (bib entry)

6. ConForm

• "A Comparison of the Conventional and Formal Design of a Secure System Component'' P.G.Larsen, T.M.Brookes, M.A.Green, J.S.Fitzgerald. Published by "Nordic Seminar on Dependable Computing Systems 1994'' 24-26 August, Technical University of Denmark (bib entry)

• "Formal and Informal Specifications of a Secure System Component: first results in a comparative study'', J.S.Fitzgerald, P.G.Larsen, T.M.Brookes, M.A.Green. Published at "Formal Methods Europe '94: Industrial Benefit of Formal Methods", pp. 35-44, Springer-Verlag, Barcelona, October 1994 (bib entry)

• "Developing a Security-critical System using Formal and Conventional Methods." J.S. Fitzgerald, P.G. Larsen, T.M. Brookes, M.A. Green. Printed in "Applications of Formal Methods", chapter 14, M. Hinchey, J.P. Bowen (eds.), Prentice Hall International Series in Computer Science, September 1995 (bib entry).

• "Formal Modelling and Simultation in the Development of a Security-critical Message Processing System"P.G. Larsen, J.S. Fitzgerald, T.M. Brookes, M.A. Green. Prepared for "the Anglo-French workshop on Formal Methods, Modelling and Simulation for System Engineering." Paris, Februrary 1995 (bib entry).

• "Formal specification techniques in the commercial development process." J.S. Fitzgerald and P.G. Larsen. Position Papers from the Workshop on Formal Methods Application in Software Engineering Practise, International Conference on Software Engineering (ICSE-17), Seattle, 1995 (bib entry).

• "Applying Formal Specification in Industry." P.G. Larsen, J. Fitzgerald, and T. Brookes. Published in "IEEE Software" vol. 13, no. 3, May 1996 (bib entry).

• "Formal and Informal Specifications of a Secure System Component: Final Results in a comparative study." T.M. Brookes, J.S. Fitzgerald, and P.G. Larsen. Published in "FME'96: Industrial Benefit and Advances in Formal Methods", Springer-Verlag, March 1996 (bib entry).

PICGAL

• "PICGAL: Lessons Learnt from a Practical Use of Formal Specification to Develop a High Reliability Software" L.Devauchelle, P.G.Larsen and H.Voss. Published in the Proceedings of DASIA'97, Seville, Spain, May 1997 (bib entry).

• "PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System" L. Devauchelle, P.G.Larsen and H.Voss. Published in FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, Springer-Verlag, LNCS 1125, 1997 (bib entry).

7. Formal Methods in General

• "FME'93: Industrial-Strength Formal Methods."J.C.P Woodcock and P.G. Larsen (eds.), Springer-Verlag, Lecture Notes in Computer Science 670, April 1993 (bib entry)

• "Special issue on FME'93: Industrial-Strength Formal Methods.J.C.P. Woodcock and P.G. Larsen (eds.), IEEE Transaction on Software Engineering, February 21(2), 1995 (bib entry).

• "On the Industrial Value of Models", P.G. Larsen, (Invited Paper), 2nd BCS-FACS Northern Formal Methods Workshop, Springer ISBN 3-540-76215-9, Ilkley 1997 (bib entry).
• "CSK Corporation Launches VDMTools in Japan", Araki Keijiro, Dines  Bjørner and Peter Gorm Larsen, BCS (British Computer Society) electronic journal FACS FACT, October 2005 (bib entry).

• John Fitzgerald and Peter Gorm Larsen, Triumphs and Challenges for Model-Oriented Formal Methods: the VDM++ experience, ISOLA 2006. Also available as Technical Report, CS-TR-999, University of Newcastle upon Tyne, January 2007, http://www.cs.ncl.ac.uk/research/pubs/trs/papers/999.pdf. (bib entry)
• Juan Bicarregui, John Fitzgerald, Peter Gorm Larsen and Jim Woodcock, Industrial Practice in Formal Methods, Formal Methods09, November 2009 (bib entry).
• Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui and John Fitzgerald, Formal Methods: Practice and Experience, ACM Computing Surveys, October 2009 (bib entry)

8. Education

• "Two courses on VDM++ for Embedded Systems: Learning by Doing, P.G. Larsen, Formal Methods Educations Workshop, Canada, August, 2006 (bib entry).
• Peter Gorm Larsen, John Fitzgerald and Steve Riddle, Learning by Doing: Practical Courses in Lightweight Formal Methods using VDM++, FM Education workshop at FM'06. Also available as Technical Report, CS-TR-999, University of Newcastle upon Tyne, December 2006, http://www.cs.ncl.ac.uk/research/pubs/trs/papers/992.pdf (bib entry)
• Peter Gorm Larsen, John Fitzgerald and Steve Riddle, Practice-oriented courses in formal methods using VDM++, Formal Aspects of Computing journal, February 2008, http://www.springerlink.com/content/y2361818q6l4gwg6/ (bib entry)
• A Multidisciplinary Engineering Summer School in an Industrial Setting, Peter Gorm Larsen, Joáo M. Fernandes, Jacek Habel, Hanne Lehrskov, Richard J.C. Vos, Oliver Wallington and Jan Zidek, Published by the European Journal of Engineering Education, August, 2009 (bib entry).

9. Defence Interoperability

• "Untangling Technology Debates on Information Sharing and Interoperability", F.D. Jørgensen, P.G. Larsen, J.M. Stadtmueller, MILCOM'05, October 2005, New Jersey (bib entry).
• "Coalition C2 Interoperability Challenges", P.G. Larsen, 11th International Command and Control Research and Technology Symposium, September 2006, Cambridge, UK (bib entry).