An extended framework for passive asynchronous testing. (English) Zbl 1353.68052
Summary: In passive testing a monitor observes the trace (sequence of inputs and outputs) of the system under test (SUT) and checks that this trace satisfies a given property \(P\), potentially triggering a response if an incorrect behaviour is observed. Recent work has explored a variant of passive testing, in which we have a required property \(P\) of the traces of the SUT and there is a first-in-first-out (FIFO) network between the SUT and the monitor. The problem here is that the trace observed by the monitor need not be that produced by the SUT. Previous work has shown how such asynchronous passive testing can be performed if the property \(P\) is defined by a pair \((\rho, O_\rho)\) that represents the requirement that if trace \(\rho\) is produced by the SUT then the next output must be from the set \(O_\rho\). This paper generalises the previous work to the case where the property \(P\) is defined by a finite automaton.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q45 | Formal languages and automata |
Software:
PTTACReferences:
| [1] | Ammann, P.; Offutt, J., Introduction to Software Testing (2008), Cambridge University Press · Zbl 1154.68042 |
| [2] | Andrés, C.; Merayo, M. G.; Núñez, M., Formal passive testing of timed systems: theory and tools, Softw. Test. Verif. Reliab., 22, 6, 365-405 (2012) |
| [3] | Arnedo, J. A.; Cavalli, A.; Núñez, M., Fast testing of critical properties through passive testing, (15th Int. Conf. on Testing Communicating Systems. 15th Int. Conf. on Testing Communicating Systems, TestCom’03. 15th Int. Conf. on Testing Communicating Systems. 15th Int. Conf. on Testing Communicating Systems, TestCom’03, Lect. Notes Comput. Sci., vol. 2644 (2003), Springer), 295-310 · Zbl 1029.68646 |
| [4] | Bauer, A., Monitorability of omega-regular languages (2010), CoRR |
| [5] | Bauer, A.; Leucker, M.; Schallhart, C., Monitoring of real-time properties, (26th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science. 26th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’06. 26th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science. 26th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’06, Lect. Notes Comput. Sci., vol. 4337 (2006), Springer), 260-272 · Zbl 1177.68141 |
| [6] | Bauer, A.; Leucker, M.; Schallhart, C., Runtime verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol., 20, 4 (2011) |
| [7] | Bayse, E.; Cavalli, A.; Núñez, M.; Zaïdi, F., A passive testing approach based on invariants: application to the WAP, Comput. Netw., 48, 2, 247-266 (2005) · Zbl 1080.68534 |
| [8] | Camacho, M. A.; Merayo, M. G.; Medina-Bulo, I., PTTAC: passive testing tool for asynchronous systems, (10th Int. Conf. on Signal-Image Technology & Internet-Based Systems. 10th Int. Conf. on Signal-Image Technology & Internet-Based Systems, SITIS’14 (2014), IEEE Computer Society), 223-229 |
| [9] | Cavalli, A. R.; Higashino, T.; Núñez, M., A survey on formal active and passive testing with applications to the cloud, Ann. Télécommun., 70, 3-4, 85-93 (2015) |
| [10] | Che, X.; Maag, S., Passive performance testing of network protocols, Comput. Commun., 51, 36-47 (2014) |
| [11] | Clerbout, M.; Latteux, M., Semi-commutations, Inf. Comput., 73, 1, 59-74 (1987) · Zbl 0629.68078 |
| [12] | Colombo, C.; Pace, G. J.; Abela, P., Safer asynchronous runtime monitoring using compensations, Form. Methods Syst. Des., 41, 3, 269-294 (2012) · Zbl 1284.68142 |
| [13] | Dilworth, R. P., A decomposition theorem for partially ordered sets, Ann. Math., 51, 1, 161-166 (1950) · Zbl 0038.02003 |
| [14] | Hierons, R. M.; Bogdanov, K.; Bowen, J. P.; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M.; Kapoor, K.; Krause, P.; Luettgen, G.; Simons, A. J.H.; Vilkomir, S.; Woodward, M. R.; Zedan, H., Using formal specifications to support testing, ACM Comput. Surv., 41, 2 (2009) |
| [15] | Hierons, R. M.; Merayo, M. G.; Núñez, M., Testing from a stochastic timed system with a fault model, J. Log. Algebraic Program., 78, 2, 98-115 (2009) · Zbl 1161.68026 |
| [16] | Hierons, R. M.; Merayo, M. G.; Núñez, M., Passive testing with asynchronous communications, (IFIP 33rd Int. Conf. on Formal Techniques for Distributed Systems. IFIP 33rd Int. Conf. on Formal Techniques for Distributed Systems, FMOODS/FORTE’13. IFIP 33rd Int. Conf. on Formal Techniques for Distributed Systems. IFIP 33rd Int. Conf. on Formal Techniques for Distributed Systems, FMOODS/FORTE’13, Lect. Notes Comput. Sci., vol. 7892 (2013), Springer), 99-113 |
| [17] | Ilie, L.; Yu, S., Follow automata, Inf. Comput., 186, 1, 140-162 (2003) · Zbl 1059.68063 |
| [18] | Kupferman, O.; Vardi, M. Y., Model checking of safety properties, (11th Int. Conf. on Computer Aided Verification. 11th Int. Conf. on Computer Aided Verification, CAV’99. 11th Int. Conf. on Computer Aided Verification. 11th Int. Conf. on Computer Aided Verification, CAV’99, Lect. Notes Comput. Sci., vol. 1633 (1999), Springer), 172-183 · Zbl 1046.68597 |
| [19] | Kupferman, O.; Vardi, M. Y., Model checking of safety properties, Form. Methods Syst. Des., 19, 3, 291-314 (2001) · Zbl 0995.68061 |
| [20] | Latvala, T., Efficient model checking of safety properties, (10th Int. SPIN Workshop on Model Checking of Software. 10th Int. SPIN Workshop on Model Checking of Software, SPIN’03. 10th Int. SPIN Workshop on Model Checking of Software. 10th Int. SPIN Workshop on Model Checking of Software, SPIN’03, Lect. Notes Comput. Sci., vol. 2648 (2003), Springer), 74-88 · Zbl 1023.68625 |
| [21] | Lee, D.; Chen, D.; Hao, R.; Miller, R. E.; Wu, J.; Yin, X., Network protocol system monitoring: a formal approach with passive testing, IEEE/ACM Trans. Netw., 14, 424-437 (2006) |
| [22] | Lee, D.; Netravali, A. N.; Sabnani, K. K.; Sugla, B.; John, A., Passive testing and applications to network management, (5th IEEE Int. Conf. on Network Protocols. 5th IEEE Int. Conf. on Network Protocols, ICNP’97 (1997), IEEE Computer Society), 113-122 |
| [23] | Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebraic Program., 78, 5, 293-303 (2009) · Zbl 1192.68433 |
| [24] | Mazurkiewicz, A., Trace theory, (Petri Nets: Applications and Relationships to Other Models of Concurrency. Petri Nets: Applications and Relationships to Other Models of Concurrency, Lect. Notes Comput. Sci., vol. 255 (1987), Springer), 278-324 · Zbl 0633.68051 |
| [25] | Merayo, M. G.; Núñez, A., Passive testing of communicating systems with timeouts, Inf. Softw. Technol., 64, 19-35 (2015) |
| [26] | Myers, G. J., The Art of Software Testing (2004), John Wiley and Sons |
| [27] | Nguyen, H. N.; Poizat, P.; Zaïdi, F., Online verification of value-passing choreographies through property-oriented passive testing, (14th Int. Symposium on High-Assurance Systems Engineering. 14th Int. Symposium on High-Assurance Systems Engineering, HASE’12 (2012), IEEE Computer Society), 106-113 |
| [28] | Núñez, M., Algebraic theory of probabilistic processes, J. Log. Algebraic Program., 56, 1-2, 117-177 (2003) · Zbl 1048.68057 |
| [29] | Tarjan, R. E., Depth-first search and linear graph algorithms, SIAM J. Comput., 1, 2, 146-160 (1972) · Zbl 0251.05107 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
