| DMU logo

Dr Ben Moszkowski

Job: Senior Research Fellow

Faculty: Technology

School/department: School of Computer Science and Informatics

Research group(s): Software Technology Research Laboratory

Address: De Montfort University, The Gateway, Leicester, LE1 9BH, United Kingdom

T: +44 (0)116 207 8480

E: benm@dmu.ac.uk

W: www.dmu.ac.uk/strl/

 

Personal profile

My PhD research over thirty years ago at Stanford University introduced the formalism Interval Temporal Logic (ITL), originally intended for use in Computer Hardware Verification. I subsequently showed how ITL could serve as the basis of a Programming Language for Executable Specifications and additionally as a framework for Compositional Reasoning about Concurrency. I have also done work on Complete Axiom Systems for versions of ITL and investigated Hierarchical Connections between it and other temporal logics. My recent work, which builds on research over the last two decades, concerns new compositional properties of ITL and associated techniques for Time Reversal. These involve remarkably simple mathematics and are also relevant to some other standard temporal logics, yet were apparently not known until now. In hindsight, the core ITL formalism has changed rather little since the time of my PhD dissertation, but the body of results concerning its theory and application have continued to expand, sometimes in quite surprising ways!

Here is a link to more information about ITL: http://www.tech.dmu.ac.uk/STRL/ITL/|

Almost since its inception, ITL has inspired and influenced others and been used and adapted in research undertaken around the world. This process has in turn also helped contribute to a greater understanding about ITL itself. Below is a list of various projects:

HOL interactive theorem prover, originally developed by Professor M. C. J. Gordon, FRS. 

Provable Correct Systems (ProCoS) European research projects headed by Prof Sir C. A. R. Hoare, FRS. A central formalism in ProCoS was the Duration Calculus, a real-time/hybrid variant of ITL developed by Prof Zhou Chaochen (previously Director of UNU-IIST in Macau, and now a member of the Chinese Academy of Sciences) and others.

IEEE Standard 1647 (published in 2006 and revised in 2008, with a further revision in the works) for the Functional Verification Language 'e'. This includes the assertion language temporal 'e', which has been influenced by Interval Temporal Logic and the Tempura programming language based on it. 

MetateM, a framework for executable temporal formulas developed by Profs H. Barringer, M. Fisher, D. Gabbay and others.

ITL-based formalisation of Security Requirements and Access Control Policies by A. Cau, H. Janicke, F. Siewe and H. Zedan at DMU. Some of this research has been funded through the Data Information Fusion Defence Technology Centre (DIF DTC), which was headed, on behalf of the UK Ministry of Defence (MOD), by General Dynamics UK. It was established to form a research community of excellence in the field of data and information fusion. De Montfort University was a member of the consortium and so were BT, QinetiQ, Imperial College and the Universities of Bristol, Cardiff, Cambridge, Southampton, Surrey and Cranfield. 

The KIV interactive theorem prover at the University of Augsburg, Germany. Applications involving ITL include showing the correctness of the following:

  • Lock-free algorithms using rely-guarantee conditions
  • Safety critical systems represented with Statecharts.

Projection Temporal Logic, an ITL-based notation investigated by Prof Z Duan and his group at Xidian University, Xi'an, China for reasoning about concurrent programs.

Three recent textbooks about temporal logic include material on ITL and other research influenced by it: 

   Real-Time Systems: Formal Specification and Automatic Verification.
   E.-R. Olderog and H. Dierks, Cambridge University Press, 2008.

   Temporal Logic and State Systems.
   F. Kröger and S. Merz, Springer, 2008. 

   An Introduction to Practical Formal Methods Using Temporal Logic.
   M. Fisher, John Wiley & Sons, Ltd., 2011.

The first of these extensively uses the Duration Calculus as the core logical formalism. Its co-author Prof. E.-R. Olderog is a 1994 recipient of the Leibniz Prize of the German Research Foundation (DFG) ("The highest honour awarded in German research") and also a member of Academia Europaea.

Publications and outputs 

Click here to see a full listing of Ben Moszkowski's publications and outputs.|

Key research outputs

Moszkowski, B. (1985) A temporal logic for multilevel reasoning about hardware, IEEE Computer, 18 (2), pp.10-19.

Moszkowski, B. (1986) Executing Temporal Logic Programs, Cambridge University Press.

Moszkowski, B. (2012) A complete axiom system for propositional Interval Temporal Logic with infinite time. Logical Methods in Computer Science, 8 (3), paper 10, pp. 1-56.

Moszkowski, B. (2013) Interconnections between classes of sequentially compositional temporal formulas, Information Processing Letters, 113 (9), pp. 350-353.

Moszkowski, B. (2013) Compositional reasoning using intervals and time reversal, Annals of Mathematics and Artificial Intelligence, DOI: 10.1007/s10472-013-9356-8.

Research interests/expertise

Formal Methods

Temporal Logic (especially Interval Temporal Logic)

Compositionality and Modularity

Executable Specifications

Verification

Qualifications

Bachelor of Science (Mathematics/Computer Science), University of California at Los Angeles (UCLA), California, USA, 1976, summa cum laude (i.e., “highest distinction”) with departmental honours.

PhD (Computer Science), Stanford University, California, USA, 1983.
(Supervisor: Professor Zohar Manna).

Honours and awards

Award for best paper in the formal methods track at the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), Nov., 1995.

US National Science Foundation Graduate Fellowship, 1976-1979, in recognition of demonstrated potential for significant achievements in science and engineering research.

Phi Beta Kappa, 1976. This is the oldest and most widely known academic honour society in US. It invites for induction the most outstanding arts and sciences students at leading US colleges and universities.

Membership of professional associations and societies

ACM

Conference attendance

I have given invited talks and/or papers at the following conferences, workshops and Festschrifts:

  • (Keynote talk and paper) 7th BCS-FACS Refinement Workshop, Bath, UK, 3-5 July 1996. 
  • Festschrift in honour of Prof. Dov Gabbay on his 60th birthday, 2005.
  • (Invited tutorial) Workshop on Interval Temporal Logics and Duration Calculi, 15th European Summer School in Logic Language and Information (ESSLLI 2003), Vienna, Austria, 25-29 Aug 2003. 
  • Symposium and Festschrift in honour of Prof. Zohar Manna on his 64th Birthday, Taormina, Sicily, Italy, 29 June - 4 July 2003.
  • Dagstuhl seminar #01081 on Applications of Kleene Algebra, International Conference and Research Center for Computer Science, Schloss Dagstuhl, Wadern, Germany, 18-23 February 2001. 
  • International symposium Compositionality: The Significant Difference (COMPOS'97), Bad Malente, Germany, 8-12 September 1997. This successful event was organised by W.-P. de Roever, H. Langmaack and the late A. Pnueli following my suggestion.
  • NSF/ESPRIT Hardware Synthesis and Verification Workshop, Cornell University, Ithaca, New York, USA, 15 August 1996. 
  • COS concurrency workshop, University of York, York, England, 28 May 1992.
  • Workshop on Logic Programming, Rehovot, Israel, 12 February 1986. 
  • Workshop on Formal Aspects of VLSI Design, Edinburgh, Scotland, 30 June - 2 July 1985.
  • IFIP WG 10.2/10.5 Workshop on Hardware Design Verification, Darmstadt, West Germany, 26-27 November 1984. 
  • NSF/SERC Workshop on the Semantics of Concurrency, Pittsburgh, Pennsylvania, 9-11 July 1984.

Externally funded research grants information

Interval Temporal Logic has played a significant role in all of the following research grants which I have been involved in:

  • Compositional Methods for Hardware/Software Co-design, EPSRC (GR/M32474), research grant, June '99 to November '02. De Montfort University (with Prof. H. Zedan, A. Cau, R. Hale and J. Dimitrov) and Oxford University (Sir Prof. C.A.R. Hoare, FRS, and after his retirement from Oxford, M. Spivey, and M. Manjunathaiah). 
  • A Compositional Approach to the Specification of Systems using ITL and Tempura, EPSRC (GR/K25922), research grant, 1995 to 1998. Newcastle University (with J.N. Coleman and Li Xiao Shan) and De Montfort University (Prof. H. Zedan).
  • Analyzing Hardware-Software Systems Using Interval Temporal Logic, SERC (GR/J10631), research grant, 1992 to 1994. Newcastle University (with C. Holt and Z. Duan).
  • Temporal Logic Analysis of Real Digital Systems, SERC (GR/C40022), research grant, January '83 to December '85. Cambridge University (with Prof. M. J. C. Gordon, FRS).

Professional esteem indicators

Invited talk at BCS-FACS Evening Seminar, London, 2007.

Invited talk at Belgian national seminar organised by Centre Fédéré en Vérification (Federal Centre for Verification), Brussels, Belgium, 2007.

Editorial boards/reviewing activities:

Guest editor together with D. Guelev and M. Leucker of special issue of Annals of Mathematics and Artificial Intelligence (Springer) on interval temporal logics, 2012-present.

19th International Symposium on Temporal Representation and Reasoning (TIME'12), Leicester, 12-14 September '12.  General chair and programme co-chair.

18th International Symposium on Temporal Representation and Reasoning (TIME'11), Lübeck, Germany, 12-14 September '11. Organised with D. Guelev an invited special track on interval temporal logics, also PC member.

I have reviewed submissions for the following journals:

ACM Computing Surveys
ACM Transactions on Programming Languages and Systems
ACM Transactions on Software Engineering and Methodology
The Computer Journal
Computing and Informatics
Formal Aspects of Computing
Information and Control
IEE Software Engineering Journal
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
IEEE Transactions on Computers
IEEE Transactions on Software Engineering
International Journal of Software and Informatics
Journal of Automated Reasoning
Journal of the ACM
Journal of Logic and Computation
Notre Dame Journal of Formal Logic
Software Engineering and Practice
Software Testing, Verification and Reliability
Theoretical Computer Science

I have reviewed submissions for the following conferences:

CONCUR
Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT)
Logic for Programming Artificial Intelligence and Reasoning (LPAR)
International Colloquium on Theoretical Aspects of Computing (ICTAC)
International Symposium on Mathematical Foundations of Computer Science (MFCS)
Symposium on Logical Foundations of Computer Science (LFCS)
Theory and Applications of Model of Computation (TAMC).

Case studies

IEEE standard 1647 (published in 2006 and revised in 2008, with a further revision in the works) for the Functional Verification Language 'e'. This includes the assertion language temporal 'e' that has been influenced by Interval Temporal Logic and the Tempura programming language based on it. The company Cadence, which plays a significant role in software tools for computer-aided design (CAD), creates and markets "Specman" products based on the standard.

Search Who's Who

 
News target area image
News

DMU is a dynamic university, read about what we have been up to in our latest news section.

Events target area image
Events

At DMU there is always something to do or see, check out our events for yourself.

Mission and vision target area image
Mission and vision

Read about our mission and vision and how these create a supportive and exciting learning environment.