Abstract
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.
Research supported in part by the CICYT project TIC 2000-0701-C02-01. This research was carried out while the first author was visiting the GET-INT. He would like to thank Ana Cavalli for helpful discussions on testing and for her financial support under the Platonis project.
Chapter PDF
Similar content being viewed by others
References
R. Alur and D. Dill.A theory of timed automata.Theoretical Computer Science, 126:183–235,1994.
K.J. Arrow.Social Choice and Individual Values.Wiley,2nd edition,1963.
M. Barbuceanu and W.K. Lo.Multi-attribute utility theoretic negotiation for electronic commerce.In AMEC 2000,LNAI2003,pages 15–30.Springer,2001.
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.
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.
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.
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.
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.
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.
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.
ISO/IEC.ODP Trading Function.Draft International Standard 13235,ISO-Information Processing Systems,1995.
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.
D. Lee and M. Yannakakis.Principles and methods of testing finite state machines:A survey.Proceedings of the IEEE,84(8):1090–1123,1996.
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.
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.
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.
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.
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.
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: http://dalila.sip.ucm.es/~manolo/papers/pamr.ps.
M. Núñez and I. Rodríguez.Applying PAMR to the management of software projects:Humans as resources,2002.Submitted for publication.
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.
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.
L. Rasmusson and S. Janson.Agents,self-interest and electronic markets.Knowledge Engineering Review,14(2):143–150,1999.
J. Springintveld, F. Vaandrager,and P.R. D’Argenio.Testing timed automata.Theoretical Computer Science,254(1–2):225–257,2001.
J. Tretmans.Test generation with inputs,outputs and repetitive quiescence.Software Concepts and Tools,17(3):103–120,1996.
J. Tretmans. Testing concurrent systems:A formal approach.In CONCUR’ 99, LNCS1664,pages 46–65.Springer,1999.
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.
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
Núñez, M., Rodríguez, I. (2002). Encoding PAMR into (Timed) EFSMs. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_1
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive