Encoding PAMR into (Timed) EFSMs

  • Manuel Núñez
  • Ismael Rodríguez
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


In this paper we show how the formal framework introduced in PAMR (Process Algebra for the Management of Resources)can be included into a notion of Extended Finite State Machines (in short EFSM). First, we give the definition of process. Following the lines of PAMR ,a process consists not only of information about its behavior but also of information about the preference for resources. This information will be encoded into a model based on EFSMs. In contrast with the original definition of PAMR, a notion of time is included in our processes,that is, transitions take time to be performed. Systems are defined as the composition of several processes. We present different implementation relations, depending on the interpretation of time, and we relate them. Finally,we study how tests cases are defined and applied to implementations.


  1. 1.
    R. Alur and D. Dill.A theory of timed automata.Theoretical Computer Science, 126:183–235,1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    K.J. Arrow.Social Choice and Individual Values.Wiley,2nd edition,1963.Google Scholar
  3. 3.
    M. Barbuceanu and W.K. Lo.Multi-attribute utility theoretic negotiation for electronic commerce.In AMEC 2000,LNAI2003,pages 15–30.Springer,2001.Google Scholar
  4. 4.
    P. Brémond-Grégoire and I. Lee.A process algebra of communicating shared resources with dense time and priorities. Theoretical Computer Science,189(1–2):179–219,1997.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    E. Brinksma, G. Scollo,and C. Steenbergen.LOTOS specifications,their implementations and their tests.In Protocol Specification, Testing and Verification VI, pages 349–360.North Holland,1986.Google Scholar
  6. 6.
    A. Cavalli, J.P. Favreau,and M. Phalippou.Standardization of formal methods in conformance testing of communication protocols.Computer Networks and ISDN Systems,29:3–14,1996.CrossRefGoogle Scholar
  7. 7.
    D. Clarke and I. Lee.Automatic generation of tests for timing constraints from requirements. In 3rd Workshop on Object-Oriented Real-Time Dependable Systems, 1997.Google Scholar
  8. 8.
    M. Dastani, N. Jacobs, C.M. Jonker,and J. Treur.Modelling user preferences and mediating agents in electronic commerce.In Agent Mediated Electronic Commerce, LNAI1991,pages 163–193.Springer,2001.Google Scholar
  9. 9.
    D. deFrutos-Escrig, L.F. Llana-Díaz, and M. Núñez. Friendly testing as a conformance relation.In Formal Description Techniques for Distributed Systems and Communication Protocols (X),and Protocol Specification,Testing,and Verification (XVII),pages 283–298.Chapman & Hall,1997.Google Scholar
  10. 10.
    T. Higashino, A. Nakata, K. Taniguchi,and A. Cavalli.Generating test cases for a timed I/O automaton model.In 12th Workshop on Testing of Communicating Systems,pages 197–214.Kluwer Academic Publishers,1999.Google Scholar
  11. 11.
    ISO/IEC.ODP Trading Function.Draft International Standard 13235,ISO-Information Processing Systems,1995.Google Scholar
  12. 12.
    S. Kalyanasundaram, E.K.P. Chong, and N.B. Shroff Optimal resource allocation in multi-class networks with user-specified utility functions.Computer Networks, 38:613–630,2002.CrossRefGoogle Scholar
  13. 13.
    D. Lee and M. Yannakakis.Principles and methods of testing finite state machines:A survey.Proceedings of the IEEE,84(8):1090–1123,1996.Google Scholar
  14. 14.
    L.P. Lima and A. Cavalli.A pragmatic approach to generating tests sequences for embedded systems. In 10th Workshop on Testing of Communicating Systems, pages 288–307.Chapman &Hall,1997.Google Scholar
  15. 15.
    N.López, M.Núñez, I. Rodríguez, and F. Rubio.A formal framework for e-barter based on microeconomic theory and process algebras. In Innovative Internet Computer Systems,LNCS2346,pages 217–228.Springer,2002.CrossRefGoogle Scholar
  16. 16.
    N. López, M. Núñez, I. Rodrǵuez,and F. Rubio.Including malicious agents into a collaborative learning environment. In 8th Intelligent Tutoring Systems, LNCS 2363,pages 51–60.Springer,2002.Google Scholar
  17. 17.
    S.H. Low and D.E. Lapsley.Optimization flow control I:Basic algorithm and convergence.IEEE/ACM Transactions on Networking,7(6):861–875,1999.CrossRefGoogle Scholar
  18. 18.
    D. Mandrioli, S. Morasca,and A. Morzenti.Generating test cases for real time systems from logic specifications.ACM Trans.on Computer Systems,13(4):356–398,1995.CrossRefGoogle Scholar
  19. 19.
    M. Núñez and I. Rodríguez.PAMR:A process algebra for the management of resources in concurrent systems. In FORTE 2001,pages 169–185.Kluwer AcademicPublishers,2001.An extended version of this paper is available at:
  20. 20.
    M. Núñez and I. Rodríguez.Applying PAMR to the management of software projects:Humans as resources,2002.Submitted for publication.Google Scholar
  21. 21.
    A. Petrenko, N. Yevtushenko,and G. vonBochmann.Fault models for testing in context.In Formal Description Techniques for Distributed Systems and Communication Protocols (IX),and Protocol Specification,Testing,and Verification (XVI), pages 163–178.Chapman &Hall,1996.Google Scholar
  22. 22.
    A. Petrenko, N. Yevtushenko, and G. vonBochmann.Testing deterministic implementations from their nondeterministic specifications.In 9th Workshop on Testing of Communicating Systems,pages 125–140.Chapman &Hall,1996.Google Scholar
  23. 23.
    L. Rasmusson and S. Janson.Agents,self-interest and electronic markets.Knowledge Engineering Review,14(2):143–150,1999.CrossRefGoogle Scholar
  24. 24.
    J. Springintveld, F. Vaandrager,and P.R. D’Argenio.Testing timed automata.Theoretical Computer Science,254(1–2):225–257,2001.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    J. Tretmans.Test generation with inputs,outputs and repetitive quiescence.Software Concepts and Tools,17(3):103–120,1996.Google Scholar
  26. 26.
    J. Tretmans. Testing concurrent systems:A formal approach.In CONCUR’ 99, LNCS1664,pages 46–65.Springer,1999.Google Scholar
  27. 27.
    H. Yaiche, R.R. Mazumdar,and C. Rosenberg.A game theoretic framework for bandwith allocation and pricing in broadband networks.IEEE/ACM Transactions on Networking,8(5):667–678,2000.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Manuel Núñez
    • 1
  • Ismael Rodríguez
    • 1
  1. 1.Dept.Sistemas Informáticos y ProgramaciónUniversidad Complutense de MadridMadridSpain

Personalised recommendations