Formal correctness of a passive testing approach for timed systems
| dc.book.title | ICSTW 2009: IEEE International Conference on Software Testing, Verification, and Validation Workshops | |
| dc.contributor.author | García Merayo, María De Las Mercedes | |
| dc.contributor.author | Andrés Sánchez, César | |
| dc.contributor.author | Núñez García, Manuel | |
| dc.date.accessioned | 2023-06-20T05:44:11Z | |
| dc.date.available | 2023-06-20T05:44:11Z | |
| dc.date.issued | 2009-04 | |
| dc.description | International Conference on Software Testing, Verification, and Validation Workshops. APR 01-04, 2009. Denver, CO. | |
| dc.description.abstract | In this paper we extend our previous work on passive testing of timed systems to establish a formal criterion to determine correctness of an implementation under test. In our framework, an invariant expresses the fact that if the implementation under test performs a given sequence of actions, then it must exhibit a behavior in a lapse of time reflected in the invariant. In a previous paper we gave an algorithm to establish the correctness of an invariant with respect to a specification. In this paper we continue the work by providing an algorithm to check the correctness of a log, recorded form the implementation under test, with respect to an invariant. We show the soundness of our method by relating it to an implementation relation. In addition to the theoretical framework we have developed a tool, called PASTE, that facilitates the automation of our passive testing approach. | |
| 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/15629 | |
| dc.identifier.doi | 10.1109/ICSTW.2009.34 | |
| dc.identifier.isbn | 978-0-7695-3671-2 | |
| dc.identifier.officialurl | http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=4976372 | |
| dc.identifier.relatedurl | http://www.ieee.org/ | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/45319 | |
| dc.language.iso | eng | |
| dc.page.total | 76 | |
| dc.publication.place | LOS ALAMITOS | |
| dc.publisher | IEEE Comp Soc | |
| dc.relation.projectID | TIN2006-15578-C02-01 | |
| dc.rights.accessRights | open access | |
| dc.subject.cdu | 519.8 | |
| dc.subject.keyword | Finite-state machines | |
| dc.subject.ucm | Matemáticas (Matemáticas) | |
| dc.subject.ucm | Investigación operativa (Matemáticas) | |
| dc.subject.unesco | 12 Matemáticas | |
| dc.subject.unesco | 1207 Investigación Operativa | |
| dc.title | Formal correctness of a passive testing approach for timed systems | |
| dc.type | book part | |
| dcterms.references | C. Andrés, M.G. Merayo, and M. Núñez. Passive testing of timed systems. In 6th Int. Symposium on Automated Technology for Verification and Analysis, ATVA’08, LNCS 5311, pages 418–427. Springer, 2008. An extended version is available at http://kimba.mat.ucm.es/manolo/papers/atva08- passive-extended.pdf. C. Andrés, M.G. Merayo, and M. Núñez. Passive testing of stochastic timed systems. In 2nd Int. Conf. on Software Testing, Verification, and Validation, ICST’09 (in press). IEEE Computer Society Press, 2009. J.A. Arnedo, A. Cavalli, and M. Núñez. Fast testing of critical properties through passive testing. In 15th Int. Conf. on Testing Communicating Systems, Test- Com’03, LNCS 2644, pages 295–310. Springer, 2003. J.M. Ayache, P. Azema, and M. Diaz. Observer: A concept for on-line detection of control errors in concurrent systems. In 9th Symposium on Fault-Tolerant Computing, 1979. E. Bayse, A. Cavalli, M. Núñez, and F. Zaïdi. A passive testing approach based on invariants: Application to theWAP. Computer Networks, 48(2):247–266, 2005. E. Brinksma and J. Tretmans. Testing transition systems: An annotated bibliography. In 4th Summer School on Modeling and Verification of Parallel Processes, MOVEP’00, LNCS 2067, pages 187–195. Springer, 2001. A. Cavalli, C. Gervy, and S. Prokopenko. New approaches for passive testing using an extended finite state machine specification. Information and Software Technology, 45:837–852, 2003. D. Clarke and I. Lee. Automatic generation of tests for timing constraints from requirements. In 3rd Workshop on Object-Oriented Real-Time Dependable Systems, WORDS’97, pages 199–206. IEEE Computer Society Press, 1997. A. En-Nouaary, R. Dssouli, and F. Khendek. Timed Wp-method: Testing real time systems. IEEE Transactions on Software Engineering, 28(11):1024–1039, 2002. S.C.P.F. Fabbri, J.C. Maldonado, T. Sugeta, and P.C. Masiero.Mutation testing applied to validate specifications based on statecharts. In 10th IEEE Int. Symposium on Software Reliability Engineering, ISSRE’99, pages 210–219. IEEE Computer Society Press, 1999. A. Hessel, K.G. Larsen, M. Mikucionis, B. Nielsen, P. Pettersson, and A. Skou. Testing real-time systems using UPPAAL. In Formal Methods and Testing, LNCS 4949, pages 77–117. Springer, 2008. R.M. Hierons, K. Bogdanov, J.P. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. Krause, G. Luettgen, A.J.H Simons, S. Vilkomir, M.R. Woodward, and H. Zedan. Using formal methods to support testing. ACM Computing Surveys, 41(2), 2009. R.M. Hierons and M. G. Merayo. Mutation testing from probabilistic finite state machines. In 3rd Workshop on Mutation Analysis, Mutation’07, pages 141– 150. IEEE Computer Society Press, 2007. T. Higashino, A. Nakata, K. Taniguchi, and A. Cavalli. Generating test cases for a timed I/O automaton model. In 12th Int. Workshop on Testing of Communicating Systems, IWTCS’99, pages 197–214. Kluwer Academic Publishers, 1999. J. Huo and A. Petrenko. On testing partially specified IOTS through lossless queues. In 16th Int. Conf. on Testing Communicating Systems, TestCom’04, LNCS 2978, pages 76–94. Springer, 2004. D. Lee and M. Yannakakis. Principles and methods of testing finite state machines: A survey. Proceedings of the IEEE, 8(8):1090–1123, 1996. D. Mandrioli, S. Morasca, and A. Morzenti. Generating test cases for real time systems from logic specifications. ACM Transactions on Computer Systems, 13(4):356–398, 1995. M.G. Merayo, M. Núñez, and I. Rodríguez. Extending EFSMs to specify and test timed systems with action durations and timeouts. IEEE Transactions on Computers, 57(6):835–848, 2008. M.G. Merayo, M. Núñez, and I. Rodríguez. Formal testing from timed finite state machines. Computer Networks, 52(2):432–460, 2008. R. Nilsson, J. Offutt, and J. Mellin. Test case generation for mutation-based testing of timeliness. In 2nd Workshop on Model Based Testing, MBT’06, pages 97–114. Electronic Notes in Theoretical Computer Science 164(4), 2006. J. Offutt. A practical system for mutation testing: Help for the common programmer. In 7th International Test Conference, ITC’94, pages 824–830. IEEE Computer Society Press, 1994. A. Petrenko. Fault model-driven test derivation from finite state models: Annotated bibliography. In 4th Summer School on Modeling and Verification of Parallel Processes, MOVEP’00, LNCS 2067, pages 196– 205. Springer, 2001. J. Springintveld, F. Vaandrager, and P.R. D’Argenio. Testing timed automata. Theoretical Computer Science, 254(1-2):225–257, 2001. Previously appeared as Technical Report CTIT-97-17, University of Twente, 1997. T. Sugeta, J.C. Maldonado, and W.E. Wong. Mutation testing applied to validate SDL specifications. In 16th IFIP Int. Conf. on Testing of Communicating Systems,TestCom’04, LNCS 2978, pages 193–208. Springer, 2004. J. Tretmans. Testing concurrent systems: A formal approach. In 10th Int. Conf. on Concurrency Theory, CONCUR’99, LNCS 1664, pages 46–65. Springer, 1999. M. Utting and B. Legeard. Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, 2007. | |
| dspace.entity.type | Publication | |
| relation.isAuthorOfPublication | 28ca46b8-d1eb-42e6-a6e2-f31b193b055b | |
| relation.isAuthorOfPublication | 26825d32-1d0a-4bbb-b145-e014e22f1a88 | |
| relation.isAuthorOfPublication.latestForDiscovery | 26825d32-1d0a-4bbb-b145-e014e22f1a88 |
Download
Original bundle
1 - 1 of 1
