Advertisement

Applicative Modelling with RAISE

  • Chris George
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4710)

Abstract

In this chapter we provide an introduction to the RAISE Specification Language and to the RAISE method. We concentrate on the applicative style of RAISE, the style most commonly used initially in development.

We also describe two examples. The first is a simple communication system that allows the transmission of messages with the possibility of higher priority messages overtaking others. The example illustrates the use of abstract initial specification to capture vital properties, and of more detailed concrete specification to describe a model having those properties. The second example is a control system of a lift, and illustrates the use of model checking to gain confidence in a RAISE model.

Keywords

Model Check Transition System Applicative Modelling Priority Queue Type Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    George, C., Prehn, S.: The RAISE Tools Users Guide. LaCoS Report DOC/7, Computer Resources International A/S (1992)Google Scholar
  2. 2.
    Chalmers, D., Dandanell, B., Gørtz, J., Pedersen, J.S., Zierau, E.: Using RAISE — First Impressions From a LaCoS User Trial. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 551, Springer, Heidelberg (1991)Google Scholar
  3. 3.
    Milne, R.: The Formal Basis for the RAISE Specification Language. In: Semantics of Specification Languages. Workshops in Computing, Springer, Heidelberg (1993)Google Scholar
  4. 4.
    Bolignano, D., Debabi, M.: On the Semantic Foundations of RSL: a Concurrent, Functional and Imperative Specification Language. In: Proceedings of FORTE 1993, Boston University (1993)Google Scholar
  5. 5.
    RAISE Method Group, T.: The RAISE Development Method. BCS Practitioner Series. Prentice Hall (1995), available by ftp from ftp://ftp.iist.unu.edu/pub/RAISE/method_book
  6. 6.
    RAISE Language Group, T.: The RAISE Specification Language. BCS Practitioner Series. Prentice Hall (1992), available from Terma A/S. Contact jnp@terma.comGoogle Scholar
  7. 7.
    Dang Van, H., George, C., Janowski, T., Moore, R.: Specification Case Studies in RAISE. In: FACIT, Springer, Heidelberg (2002), available by ftp from ftp://ftp.iist.unu.edu/pub/RAISE/case_studies Google Scholar
  8. 8.
    Jones, C.B., Middelburg, K.: A typed logic of partial functions reconstructed classically. Acta Informatica 31(5), 399–430 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Cheng, J., Jones, C.: On the usability of logics which handle partial functions. In: Morgan, C., Woodcock, J. (eds.) Proceedings of the Third Refinement Workshop, Springer, Heidelberg (1990)Google Scholar
  10. 10.
    Jones, C., Shaw, R.: Case Studies in Systematic Software Development. Prentice Hall International, Englewood Cliffs (1990)zbMATHGoogle Scholar
  11. 11.
    Guttag, J.V., Horning, J.J. (eds.): Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer, Heidelberg (with Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.) (1993)Google Scholar
  12. 12.
    Mosses, P.D.: CASL: A Guided Tour of its Design. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 216–240. Springer, Heidelberg (1999)Google Scholar
  13. 13.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)Google Scholar
  14. 14.
    Abrial, J.R.: The B-Book. Cambridge University Press, Cambridge (1996)zbMATHGoogle Scholar
  15. 15.
    Aichernig, B.K.: Test-design through abstraction, a systematic approach based on the refinement calculus. Journal of Universal Computer Science (J.UCS) 7(8) (2001)Google Scholar
  16. 16.
    Hörl, J., Aichernig, B.K.: Validating voice communication requirements using lightweight formal methods. IEEE Software, 21–27 (May/June 2000)Google Scholar
  17. 17.
    Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)CrossRefGoogle Scholar
  18. 18.
    Bakar, B.A., Janowski, T.: Automated Result Verification with AWK. Technical Report 205, UNU-IIST, P.O. Box 3058, Macau (June 2000) (presented at and published in the proceedings of the 6th IEEE International Conference on Engineering of Complex Computer Systems, Tokyo, Japan, IEEE Computer Society Press (September 2000))Google Scholar
  19. 19.
    ChaoChen, Z., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Proc. Letters 40(5) (1992)Google Scholar
  20. 20.
    George, C., Yong, X.: An Operational Semantics for Timed RAISE. Technical Report 149, UNU-IIST. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, Springer, Heidelberg (1999)Google Scholar
  21. 21.
    Li, L., Jifeng, H.: Towards a Denotational Semantics of Timed RSL using Duration Calculus. Technical Report 161, UNU-IIST, P.O.Box 3058, Macau (April 1999) (publication by Chinese Journal of Advanced Software Research (2000))Google Scholar
  22. 22.
    Li, L., Jifeng, H.: A Denotational Semantics of Timed RSL using Duration Calculus. Technical Report 168, UNU-IIST, P.O.Box 3058, Macau (July 1999) (presented at and published in the proceedings of The Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), part of the federated 1999 International Computer Congress, December 13 - 15, 1999, Hong Kong, pp. 492–503. IEEE Computer Society Press (1999))Google Scholar
  23. 23.
    Plotkin, G.: A structured approach to operational semantics. Technical report, Comp. Sci. Dept., Univ. of Edinburgh (1981)Google Scholar
  24. 24.
    George, C.: RAISE Tools User Guide. Technical Report 227, UNU-IIST, P.O. Box 3058, Macau (February 2001), the tools are available from http://www.iist.unu.edu
  25. 25.
    Schroër, F.W.: The GENTLE Compiler Construction System. R. Oldenbourg (1997), available from http://www.first.gmd.de/gentle/
  26. 26.
    Guttag, J.: Abstract data types and the development of data structures. CACM 20(6) (June 1977)Google Scholar
  27. 27.
    Perna, J.I., George, C.: Model checking RAISE specifications. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau (December 2005)Google Scholar
  28. 28.
    de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Chris George
    • 1
  1. 1.United Nations University International Institute for Software Technology (UNU-IIST), PO Box 3058, Macao SARChina

Personalised recommendations