Abstract
Modes are a natural abstract way of structuring the behaviour of complex systems. The different ways in which a system can operate are associated with different modes, and transitions link modes to form mode-machines. However, mode-machines need a precise semantics if they are to be used for specifying the behaviour of critical systems. This paper analyses the possible relationships between modes and states. A number of concurrent systems described using MASCOT are considered, and their mode-based behaviour is used to motivate the semantics of a new real-time mode-machine notation, RTMMs. It is argued that RTMMs should not behave like abstract state-machines. A list of concurrent transactions is associated with each RTMM mode, and a notation is given for specifying their timing properties. RTMM transactions need not terminate when the central mode-controller switches mode, thus capturing the asynchronous way in which large systems respond to mode changes. RTMMs are given a proof-theoretic semantics using many-sorted logic, extended with the RTL occurrence relation, Θ.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Audsley, N., Burns, A., Richardson, M., Tindall, K. and Wellings, A.J.: ‘Applying New Scheduling Theory to Static Priority Pre-emptive Scheduling', Softw. Eng. J., 1993, 8, (5), pp. 284–292
Armstrong, J.M.: ‘Aspects of Gradualistic Mode Transition Systems', Technical Report DCSC/TR/95/8, University of York, June 1995
Arnold, A.: ‘Finite Transition Systems', Prentice-Hall International Series in Computer Science, 1994
Avnur, A.: ‘Finite State Machines for Real-Time Software Engineering', Comp. and Cont. Eng. J., 1990, 1, (6), pp 273–278
Broy, M., Jackson, K., and Pennington, R.: ‘A Stream Function Definition of MASCOT', Technical Report, CO5255/FTR, Issue 1.1, System Designers Software Technology Centre, March 1987
Burns, A.: ‘Preemptive Priority-Based Scheduling: An Appropriate Engineering Approach', pp. 225–248, in ‘Advances in Real-Time Systems'. Edited by S.H. Son, Prentice-Hall, 1995.
Chapman, R.: 'static Timing Analysis and Program Proof', D.Phil. Thesis, Dept. of Computer Science, University of York, March 1995
Harel, D.: ‘Statecharts: A Visual Formalism for Complex Systems', Sci. of Comput. Prog., 1987, 8, pp. 231–274
Henzinger, T.A., Manna, Z., and Pnueli, A.: ‘Timed Transition Systems', Proc. ‘Real-Time: Theory in Practice', REX Workshop June 1991, Lect. Notes Comput. Sci., 600, (Springer-Verlag, 1992)
Hopcroft, J.E., and Ullman, J.D.: ‘Introduction to Automata Theory, Languages, and Computation', Addison-Wesley Publishing Company, 1979
Jahanian, F., and Mok, A.K: ‘Safety Analysis of Timing Properties in Real-Time Systems', IEEE Trans., 1986, SE-12, (9), pp. 890–904
Jahanian, F., and Mok, A.K.: ‘Modechart: A Specification Language for Real-Time Systems', IEEE Trans., 1994, SE-20, (12), pp. 933–947
Joint IECCA and MUF Committee on MASCOT (JIMCOM): ‘The Official Handbook of MASCOT', Version 3.1, Issue 1, Crown Copyright, June 1987
Jahanian, F., Lee, R., and Mok, A.K.: 'semantics of Modechart in Real Time Logic', Proc. 21st Annual Hawaii Int. Conf. on System Science, 1988, pp. 479–489, 1988
Jahanian, F., Mok, A.K., and Stuart, D.A.: ‘Formal Specification of Real-time Systems', Technical Report TR-88-25, Department of Computer Science, University of Texas at Austin, June 1988
Joseph, M.: ‘Problems, Promises and Performance: Some Questions for Real-Time System Specification', Proc. of ‘Real-Time: Theory in Practice', REX Workshop June 1991, Lect. Notes in Comput. Sci., 600, (Springer-Verlag, 1992)
Manzano, M.: ‘Introduction to Many-Sorted Logic', in Meinke, K. and Tucker, J.V. (Ed.): ‘Many-Sorted Logic and its Applications', Wiley Professional Computing, 1993
Manna, Z., and Pnueli, A.: ‘The Temporal Logic of Reactive and Concurrent Systems: Specification', Springer-Verlag, 1992
Paynter, S.E.: ‘The Formalisation of Software Development Using MASCOT', Ph.D. Thesis, Mathematics Dept., University of Southampton, December 1993
Paynter, S.E.: ‘Relating Mode-Machines and Concurrent Designs by a Process-Algebraic Foundation', To Appear, 1996.
Simpson, H.R.: ‘The MASCOT Method', Softw. Eng. J., 1986, 1, (3), pp. 103–120
Simpson, H.R.: ‘Four-Slot Fully Asynchronous Communication Mechanism', IEE Proc. E., 1990, 137, (1), pp. 17–30
Simpson, H.R.: ‘Methodological and Notational Conventions in DORIS Real-time Networks', IED Supporting Predictable Implementation of Requirements in Timing and Safety (SPIRITS) Deliverable, 1994
Simpson, H.R.: ‘Architecture for Computer Based Systems', IEEE Workshop on the Engineering of Computer Based Systems, Stockholm, 1994
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paynter, S. (1996). Real-time mode-machines. In: Jonsson, B., Parrow, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1996. Lecture Notes in Computer Science, vol 1135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61648-9_36
Download citation
DOI: https://doi.org/10.1007/3-540-61648-9_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61648-1
Online ISBN: 978-3-540-70653-3
eBook Packages: Springer Book Archive