Extending EFSMs to specify and test timed systems with action duration and time-outs
| dc.contributor.author | García Merayo, María De Las Mercedes | |
| dc.contributor.author | Núñez García, Manuel | |
| dc.contributor.author | Rodríguez Laguna, Ismael | |
| dc.date.accessioned | 2023-06-20T09:36:22Z | |
| dc.date.available | 2023-06-20T09:36:22Z | |
| dc.date.issued | 2008-06 | |
| dc.description.abstract | In this paper, we introduce a timed extension of the extended finite state machines model. On one hand, we consider that (output) actions take time to be performed. This time may depend on several factors, such as the value of variables. On the other hand, our formalism allows us to specify time-outs. In addition to presenting our language, we develop a testing theory. First, we define 10 timed conformance relations and relate them. Second, we introduce a notion of timed test and define how to apply tests to implementations. Finally, we give an algorithm to derive sound and complete test suites with respect to the implementation relations presented in the paper. This paper represents an extended and improved version of | |
| dc.description.department | Sección Deptal. de Sistemas Informáticos y Computación | |
| dc.description.faculty | Fac. de Ciencias Matemáticas | |
| dc.description.refereed | TRUE | |
| dc.description.sponsorship | MEC | |
| dc.description.status | pub | |
| dc.eprint.id | https://eprints.ucm.es/id/eprint/15660 | |
| dc.identifier.doi | 10.1109/TC.2008.15 | |
| dc.identifier.issn | 0018-9340 | |
| dc.identifier.officialurl | http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=4433986 | |
| dc.identifier.relatedurl | http://www.ieee.org | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/50016 | |
| dc.issue.number | 6 | |
| dc.journal.title | IEEE Transactions on Computers | |
| dc.language.iso | eng | |
| dc.page.final | 848 | |
| dc.page.initial | 835 | |
| dc.publisher | Institute of Electrical and Electronics Engineers | |
| dc.relation.projectID | TIN2006-15578-C02-01 | |
| dc.relation.projectID | MRTN-CT-2003-50512/TAROT | |
| dc.rights.accessRights | restricted access | |
| dc.subject.cdu | 519.8 | |
| dc.subject.keyword | Testing and debugging | |
| dc.subject.keyword | Formal methods | |
| dc.subject.keyword | Specification techniques | |
| dc.subject.keyword | Specifying and verifying and reasoning about programs | |
| dc.subject.keyword | Automata | |
| dc.subject.keyword | Computer Science | |
| dc.subject.keyword | Hardware & Architecture | |
| dc.subject.keyword | Engineering | |
| dc.subject.keyword | Electrical & Electronic | |
| dc.subject.ucm | Investigación operativa (Matemáticas) | |
| dc.subject.unesco | 1207 Investigación Operativa | |
| dc.title | Extending EFSMs to specify and test timed systems with action duration and time-outs | |
| dc.type | journal article | |
| dc.volume.number | 57 | |
| dcterms.references | M. Merayo, M. Núñez, and I. Rodríguez, “Extending EFSMs to Specify and Test Timed Systems with Action Durations and Timeouts,” Proc. 26th IFIP WG 6.1 Int’l Conf. Formal Techniques for Networked and Distributed Systems, pp. 372-387, 2006. B. Bosik and M. Uyar, “Finite State Machine Based Formal Methods in Protocol Conformance Testing,” Computer Networks and ISDN Systems, vol. 22, pp. 7-33, 1991. D. Lee and M. Yannakakis, “Principles and Methods of Testing Finite State Machines: A Survey,” Proc. IEEE, vol. 84, no. 8, pp. 1090-1123, 1996. A. Petrenko, “Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography,” Proc. Fourth Summer School on Modeling and Verification of Parallel Processes, pp. 196- 205, 2001. E. Brinksma and J. Tretmans, “Testing Transition Systems: An Annotated Bibliography,” Proc. Fourth Summer School on Modeling and Verification of Parallel Processes, pp. 187-195, 2001. K. El-Fakih, N. Yevtushenko, and G.v. Bochmann, “FSM-Based Incremental Conformance Testing Methods,” IEEE Trans. Software Eng., vol. 30, no. 7, pp. 425-436, July 2004. I. Rodríguez, M. Merayo, and M. Núñez, “HOTL: Hypotheses and Observations Testing Logic,” J. Logic and Algebraic Programming, vol. 74, no. 2, pp. 57-93, 2008. J. Sifakis, “Use of Petri Nets for Performance Evaluation,” Proc. Third Int’l Symp. Measuring, Modelling and Evaluating Computer Systems, pp. 75-93, 1977. G. Reed and A. Roscoe, “A Timed Model for Communicating Sequential Processes,” Theoretical Computer Science, vol. 58, pp. 249-261, 1988. W. Yi, “CCS + Time = An Interleaving Model for Real Time Systems,” Proc. 18th Int’l Colloquium on Automata, Languages, and Programming, pp. 217-228, 1991. X. Nicollin and J. Sifakis, “An Overview and Synthesis on Timed Process Algebras,” Proc. Third Int’l Conf. Computer Aided Verification, pp. 376-398, 1991. J. Quemada, D.d. Frutos, and A. Azcorra, “TIC: A Timed Calculus,” Formal Aspects of Computing, vol. 5, pp. 224-252, 1993. R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994. M. Hennessy and T. Regan, “A Process Algebra for Timed Systems,” Information and Computation, vol. 117, no. 2, pp. 221-239, 1995. J. Davies and S. Schneider, “A Brief History of Timed CSP,” Theoretical Computer Science, vol. 138, pp. 243-271, 1995. J. Baeten and C. Middelburg, Process Algebra with Timing, Springer, 2002. M. Núñez and I. Rodríguez, “Conformance Testing Relations for Timed Systems,” Proc. Fifth Int’l Workshop Formal Approaches to Software Testing, pp. 103-117, 2006. J. Springintveld, F. Vaandrager, and P. D’Argenio, “Testing Timed Automata,” Theoretical Computer Science, vol. 254, no. 1-2, pp. 225- 257, 2001. R. Barbuti and L. Tesei, “Timed Automata with Urgent Transitions,” Acta Informatica, vol. 40, no. 5, pp. 317-347, 2004. B. Gebremichael and F. Vaandrager, “Specifying Urgency in Timed I/O Automata,” Proc. Third IEEE Int’l Conf. Software Eng. and Formal Methods, pp. 64-73, 2005. P.-A. Hsiung, S.-W. Lin, Y.-R. Chen, C.-H. Huang, J.-J. Yeh, H.-Y. Sun, C.-S. Lin, and H.-W. Liao, “Model Checking Timed Systems with Urgencies,” Proc. Fourth Int’l Symp. Automated Technology for Verification and Analysis, pp. 67-81, 2006. D. Clarke and I. Lee Automatic Generation of Tests for Timing Constraints from Requirements, Proc. Third Workshop Object- Oriented Real-Time Dependable Systems, pp. 199-206, 1997. T. Higashino, A. Nakata, K. Taniguchi, and A. Cavalli, “Generating Test Cases for a Timed I/O Automaton Model,” Proc. 12th Int’l Workshop Testing of Communicating Systems, pp. 197-214, 1999. A. En-Nouaary and R. Dssouli, “A Guided Method for Testing Timed Input Output Automata,” Proc. 15th Int’l Conf. Testing Communicating Systems, pp. 211-225, 2003. M. Krichen and S. Tripakis, “Black-Box Conformance Testing for Real-Time Systems,” Proc. 11th Int’l SPIN Workshop Model Checking of Software, pp. 109-126, 2004. L. Branda´n Briones and E. Brinksma, “Testing Real-Time Multi Input-Output Systems,” Proc. Seventh Int’l Conf. Formal Eng. Methods, pp. 264-279, 2005. H. Fouchal, E. Petitjean, and S. Salva, “An User-Oriented Testing of Real Time Systems,” Proc. IEEE Workshop Real-Time Embedded Systems, 2001. R. Cardell-Oliver, “Conformance Tests for Real-Time Systems with Timed Automata Specifications,” Formal Aspects of Computing, vol. 12, no. 5, pp. 350-371, 2000. R. Cardell-Oliver and T. Glover, “A Practical and Complete Algorithm for Testing Real-Time Systems,” Proc. Fifth Int’l Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 251- 260, 1998. D. Mandrioli, S. Morasca, and A. Morzenti, “Generating Test Cases for Real Time Systems from Logic Specifications,” ACM Trans. Computer Systems, vol. 13, no. 4, pp. 356-398, 1995. J. Peleska and M. Siegel, “Test Automation of Safety-Critical Reactive Systems,” South African Computer J., vol. 19, pp. 53-77, 1997. M. Núñez and I. Rodríguez, “Encoding PAMR into (timed) EFSMs,” Proc. 22nd IFIP WG 6.1 Int’l Conf. Formal Techniques for Networked and Distributed Systems, pp. 1-16, 2002. A. Petrenko and N. Yevtushenko, “Conformance Tests as Checking Experiments for Partial Nondeterministic FSM,” Proc. Fifth Int’l Workshop Formal Approaches to Software Testing, pp. 118- 133, 2006. J. Tretmans, “Test Generation with Inputs, Outputs and Repetitive Quiescence,” Software—Concepts and Tools, vol. 17, no. 3, pp. 103- 120, 1996. M. Núñez and I. Rodríguez, “Towards Testing Stochastic Timed Systems,” Proc. 23rd IFIP WG 6.1 Int’l Conf. Formal Techniques for Networked and Distributed Systems, pp. 335-350, 2003. M. Merayo, M. Núñez, and I. Rodríguez, “Implementation Relations for Stochastic Finite State Machines,” Proc. Third European Performance Eng. Workshop, pp. 123-137, 2006. | |
| dspace.entity.type | Publication | |
| relation.isAuthorOfPublication | 28ca46b8-d1eb-42e6-a6e2-f31b193b055b | |
| relation.isAuthorOfPublication | 26825d32-1d0a-4bbb-b145-e014e22f1a88 | |
| relation.isAuthorOfPublication | 28429d40-53cb-4bb3-a3f6-82ec557a34ed | |
| relation.isAuthorOfPublication.latestForDiscovery | 26825d32-1d0a-4bbb-b145-e014e22f1a88 |
Download
Original bundle
1 - 1 of 1