Information Technology Reference
In-Depth Information
We have shown that it is possible to capture relative performance require-
ments, without explicitly stating time. Since mCRL2 falls into the category of
timed process algebra's [2], it allows designers to specify real-time behaviour.
Nevertheless, we have chosen not to do so for several reasons. First, we would
like to have a fair comparison between the untimed formalisms. Second, timed
requirements tend to be complex in general and require challenging manipula-
tions on the mCRL2 models before one can verify requirements. Nevertheless,
we believe that the case study considered in this paper can be formulated in a
timed specification, and can serve as subject of study for reduction and analysis
techniques for timed systems.
References
1. Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories
of Communicating Processes. Cambridge tracts in theoretical computer science,
vol. 50. Cambridge University Press, Cambridge (2010)
2. Baeten, J.C.M., Kees Middelburg, C.A.: Process Algebra with Timing. In: EATCS
Monographs, Springer, Berlin (2002)
3. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Infor-
mation and Control 60(1-3), 109-137 (1984)
4. Bluespec: Automatic Generation of Control Logic with Bluespec SystemVerilog
(Februari 2005),
http://www.bluespec.com/forum/download.php?id=63
5. Bradfield, J.C.: Verifying Temporal Properties of Systems. In: Progress in Theo-
retical Computer Science, Birkhauser, Basel (1992)
6. Daylight, E.G., Shukla, S.K.: On the di
culties of concurrent-system design, illus-
trated with a 2
×
2 switch case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM
2009. LNCS, vol. 5850, pp. 273-288. Springer, Heidelberg (2009)
7. Groote, J.F., Keiren, J., Mathijssen, A., Ploeger, B., Stappers, F., Tankink, C.,
Usenko, Y., van Weerdenburg, M., Wesselink, W., Willemse, T., van der Wulp, J.:
The mCRL2 toolset. In: Proceedings International Workshop on Advanced Soft-
ware Development Tools and Techniques, WASDeTT 2008 (2008)
8. Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a
setting with data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp.
74-90. Springer, Heidelberg (1998)
9. Groote, J.F., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.:
The formal specification language mCRL2. In: Brinksma, E., Harel, D., Mader,
A., Stevens, P., Wieringa, R. (eds.) Methods for Modelling Software Systems
(MMOSS). Dagstuhl Seminar Proceedings, vol. 06351, Internationales Begegnungs-
und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2007)
10. Groote, J.F., Mathijssen, A.H.J., Reniers, M.A., Usenko, Y.S., van Weerdenburg,
M.J.: Analysis of distributed systems with mCRL2. In: Alexander, M., Gardner, W.
(eds.) Process Algebra for Parallel and Distributed Processing, ch. 4, pp. 99-128.
Taylor & Francis, Abington (2009)
11. Harel, D.: Statecharts: A visual formalism for complex systems. Sci. Comput. Pro-
gram. 8(3), 231-274 (1987)
