Abstract
A graphical notation for representing Timed CSP (TCSP) specifications is presented. The notation, which integrates features from a number of existing specification languages, including Statecharts, is aimed at providing the means for more easily constructing and managing large TCSP specifications, with the intention of forming the basis for tools and a methodology for applying TCSP in the large. The graphical notation extends TCSP by allowing specifications to be both processes and arbitrary predicates, thus increasing the expressiveness and applicability of the notation. An extendible tool framework, designed for the graphical notation and to be integrated with other tools, is outlined. We discuss the features of this framework, especially how it aims to support reasoning about TCSP specifications.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
L. Baresi and M. Pezzè. Towards Formalizing Structured Analysis. ACM Trans. Software Engineering and Methodology 7(1), January 1998.
T. Bolognesi, E. Najm, and P. Tilanus. G-LOTOS: a graphical language for concurrent systems. Computer Networks and ISDN Systems, 26(9):1101–1127, 1994.
G. Booch, J. Rumbaugh, and I. Jacobson. The UML User Guide. Addison-Wesley, 1999.
P. Brooke. A Timed Semantics for A Hierarchical Design Notation. DPhil thesis, Department of Computer Science, University of York; also issued as YCST 99/08.
P. Brooke, J. Jacob, and J. Armstrong. An analysis of the four-slot mechanism. In Proceedings of the BCS-FACS Northern Formal Methods Workshop, electronic Workshops in Computing. Springer-Verlag, 1996.
S. Brodsky, T. Clark, S. Cook, A. Evans, and S. Kent. Feasibility Study in Rearchitecting the UML as a Family of Languages using a Precise Meta-Modeling Approach. Technical Report of pUML Group, September 2000. Available at http://www.puml.org.
J. Sun, J.S. Dong, J. Liu, and H. Wang. Z Family on the Web with their UML Photos. Technical Report TR-A1-01, School of Computing, National University of Singapore, January 2001.
Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR 2. http://www.formal.demon.co.uk/, December 1995.
T. Green and R. Navarro. Programming plans, imagery and visual programming. In Proceedings of INTERACT’ 95, 1995.
T. Green and M. Petre. When visual programs are harder to read than textual programs. In G.C. van der Veer, M.J. Tauber, S. Bagnarola, and M. Antavolits, editors, Human-Computer Interaction: Tasks and Organisation. Proceedings of ECCE6 (6th European Conference on Cognitive Ergonomics). CUD, 1992.
J. Grundy, R. Back, and J. von Wright. Structured Calculational Proof. Formal Aspects of Computing 9(5–6), 1997.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
C. Hoare. Communicating Sequential Processes. Prentice-Hall International UK, 1985.
i-Logix. Statemate: Semantics of Statecharts.
L. Lamport. How to write a long formula. Technical Report 119, DEC SRC, December 1993.
N. Leveson, M. Heimdahl, H. Hildreth, and J. Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9):684–707, September 1994. Also Technical Report 92-106 (University of California).
S. Liu, A.J. Offutt, C. Ho-Stuart, Y. Sun, and M. Ohba. SOFL: A formal engineering methodology for industrial applications. IEEE Transactions on Software Engineering, 24(1):24–45, January 1998.
B. Meyer. Object-Oriented Software Construction (Second Edition). Prentice-Hall, 1997.
R. Paige, J. Ostroff, and P. Brooke. Principles of Modelling Language Design. Information and Software Technology, 42(10):665–675, June 2000.
R. Paige and J. Ostroff. Metamodelling and Conformance Checking with PVS. In Proc. Fundamental Aspects of Software Engineering 2001. LNCS 2029, Springer-Verlag, April 2001.
M. Petre, A. Blackwell, and T. Green. Cognitive questions in software visualisation. In J. Stasko, J. Domingue, B. Price, and M. Brown, editors, Software Visualisation: Programming as a Multi-Media Experience. MIT Press, 1997.
M. Petre. Why looking isn’t always seeing: Readership skills and graphical programming. Communications of the ACM, 38(6):33–44, June 1995.
S. Schneider. Concurrent and Real-time Systems. Wiley, 2000.
H. Simpson. Four-slot fully asynchronous communication mechanism. IEE Proceedings, 137 Part E(1):17–30, January 1990.
H. Simpson. Correctness analysis for class of asynchronous communication mechanisms. IEE Proceedings, 139 Part E(1):35–49, January 1992.
T. Systa, P. Yu, and H. Muller. Analyzing Java Software by Combining Metrics and Program Visualization. In Proc. CSMR-2000, IEEE Press, Feb. 2000.
M. von der Beeck. A comparison of Statecharts variants. In H. Langmaack, W.P. de Roever, and J. Vytopil, editors, Proceedings of the 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 128–148. Springer-Verlag, 1994.
S. Owre, N. Shankar, J. Rushby, and D. Stringer-Calvert. PVS System Guide. Computer Science Laboratory, SRI International, September 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brooke, P.J., Paige, R.F. (2002). The Design of a Tool-Supported Graphical Notation for Timed CSP. In: Butler, M., Petre, L., Sere, K. (eds) Integrated Formal Methods. IFM 2002. Lecture Notes in Computer Science, vol 2335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47884-1_17
Download citation
DOI: https://doi.org/10.1007/3-540-47884-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43703-1
Online ISBN: 978-3-540-47884-3
eBook Packages: Springer Book Archive