Advertisement

Investigating the Behaviour of PREMO Synchronizable Objects

  • G. P. Faconti
  • M. Massink
Conference paper
Part of the Eurographics book series (EUROGRAPH)

Abstract

PREMO stands for Presentation Environment for Multimedia Objects and is a major new standard under development within ISO/IEC. It addresses the creation of, presentation of and interaction with all forms of information using single or multiple media. The standard (u. d.) is currently developed using an Object Oriented approach. Such a state based specification, however, does not support conveniently the analysis of the temporal relationships occurring among operations. In this paper we model PREMO synchronizable objects defined in the standard as processes in the standardized process algebra Lotos. The approach we follow is a new way to obtain a specification in a constraint oriented style and is inspired by the Object Oriented approach. We let methods correspond to actions and values of control variables with processes. Each process consists of actions that are enabled for the value of the control variable that is modelled by the process. This style leads to Basic Lotos specifications that are directly suitable for computer assisted analysis such as model checking and simulation.

Keywords

Model Check Mode Transition Extended Finite State Machine Formal Description Technique Stop Mode 
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.
    J. Bengtsson and K. G. Larsen and F. Larson find P. Petterson and Wang Yi. UPPAAL— A Tool Suite for Automatic Verification of Real-Time Systems. In Proceedings of the 4 th DIM ACS Workshop on Verification and Control of Hybrid Systems, LNCS, October 1995.Google Scholar
  2. 2.
    C. Beraardeschi and G. Ferro. A Sample Study Exemplifying the Use of JACK. In: Proceedings Workshop on Automated Formal Methods, ENTCS, vol. 5, University of Oxford, 1996.Google Scholar
  3. 3.
    J.C. Bicarregui et al. Proof in VDM: A Practitioner’s Guide. Springer-Verlag, 1994.Google Scholar
  4. 4.
    A. Bouali and S. Gnesi and S. Larosa. The Integration Project for the JACK Environment. Bulletin of the EATCS, 54, October 1994, pp. 207 – 223.zbMATHGoogle Scholar
  5. 5.
    T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14: 25 – 59, 1987.CrossRefGoogle Scholar
  6. 6.
    R. De Nicola and A. Fantechi and S. Gnesi and G. Ristori. An action based framework for verifying logical and behavioural properties of concurrent systems. In: Proceedings 3rd International Workshop CAV’91, K. G. Larsen and A. Skou (Eds.), LNCS 575, Springer-Verlag, 1991Google Scholar
  7. 7.
    R. De Nicola and A. Fantechi and S. Gnesi and G. Ristori. Verifying Hardware Components within JACK. In: Proceedings of CHARME’95, LNCS 987, Springer- Verlag, 1995, pp. 246–260.Google Scholar
  8. 8.
    R. Duke and G. Rose and G. Smith. Object-Z: A Specification Language Advocated for the Description of StandardsTechnical Report, No. 94-45, Software Verification Research Center, Department of Computer Science, University of Queensland, 1994.Google Scholar
  9. 9.
    R. De Nicola and F. Vaandrager. Action versus State based Logics for Transition Systems. In: Semantics of Systems of Concurrent Processes, I. Guessarian (Ed.), LNCS 469, Springer-Verlag, 1990.Google Scholar
  10. 10.
    D. J. Duke and D. A. Duce and I. Herman and G. Faconti. Specifying the PREMO Synchronization Objects ERCIM Computer Graphics Network Technical Report, 02/97-R048, February, 1997. (submitted for publication)Google Scholar
  11. 11.
    G. P. Faconti and M. Massink. Using LOTOS for the evaluation of Design Options in the PREMO Standard In proceedings of the BCS-FACS Northern Formed Methods Workshop, Ilkley, July 1997, Springer-Verlag. (submitted for publication)Google Scholar
  12. 12.
    C.A.R. Hoare. Communicating Sequential Processes. In Communications of ACM, 21(8), 1978.Google Scholar
  13. 13.
    International Standards Organization ISO. Information processing systems - open systems interconnection - LOTOS - a formal description technique based on the temporal ordering of observational behaviour, 1989. ISO 8807.Google Scholar
  14. 14.
    International Standards Organization ISO. Information processing systems, computer graphics, presentation environment for multimedia objects (PREMO). ISO/IEC 14478, 1996.Google Scholar
  15. 15.
    E. Madeleine and A. Pnueli. AUTO: A Verification tool for Distributed Systems using reduction of Finite Automata Networks. Formed Description Techniques, II (S. T. Vuong, ed.), 1990, pp. 61 – 66.Google Scholar
  16. 16.
    R. Milner. Communication and Concurrency. Series in Computer Science. Prentice Hall, 1989.Google Scholar
  17. 17.
    V. Roy and R. De Simone. AUTO and Autograph. In Proceedings Workshop on Computer Aided Verification, LNCS 531, Springer-Verlag, 1990, pp. 65 – 75.Google Scholar
  18. 18.
    J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1989.Google Scholar
  19. 19.
    P. van Eijk. The Lotosphere Integrated Tool Environment LITE. In Proceedings of 4th International Conference on Formal Description Techniques. North Holland, 1991.Google Scholar
  20. 20.
    C. A. Vissers and G. Scollo and M. van Sinderen and E. Brinksma. Specification Styles in Distributed Systems Design and Verification. Theoretical Computer Science, vol. 89, 1989.Google Scholar

Copyright information

© Springer-Verlag/Wien 1997

Authors and Affiliations

  • G. P. Faconti
    • 1
  • M. Massink
    • 1
  1. 1.CNR — Istituto CNUCEPisaItaly

Personalised recommendations