Testing timed systems modeled by Stream X-machines | Software and Systems Modeling | Springer Nature Link

Testing timed systems modeled by Stream X-machines | Software and Systems Modeling | Springer Nature Link
Testing timed systems modeled by Stream X-machines
Special Section Paper
Published:
14 August 2009
Volume 10
, pages 201–217, (
2011
Cite this article
Save article
View saved research
Software & Systems Modeling
Aims and scope
Submit manuscript
Abstract
Stream X-machines have been used to specify real systems where complex data structures. They are a variety of extended finite state machine where a shared memory is used to represent communications between the components of systems. In this paper we introduce an extension of the Stream X-machines formalism in order to specify systems that present temporal requirements. We add time in two different ways. First, we consider that (output) actions take time to be performed. Second, our formalism allows to specify timeouts. Timeouts represent the time a system can wait for the environment to react without changing its internal state. Since timeous affect the set of available actions of the system, a relation focusing on the functional behavior of systems, that is, the actions that they can perform, must explicitly take into account the possible timeouts. In this paper we also propose a formal testing methodology allowing to systematically test a system with respect to a specification. Finally, we introduce a test derivation algorithm. Given a specification, the derived test suite is sound and complete, that is, a system under test successfully passes the test suite if and only if this system conforms to the specification.
This is a preview of subscription content,
log in via an institution
to check access.
Access this article
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Price includes VAT (France)
Instant access to the full article PDF.
Institutional subscriptions
Similar content being viewed by others
Testing Real-Time Systems Using Determinization Techniques for Automata over Timed Domains
Chapter
A Data-Driven Time-Series Fault Prediction Framework for Dynamically Evolving Large-Scale Data Streaming Systems
Article
09 May 2022
Multiple Mutation Testing for Timed Finite State Machine with Timed Guards and Timeouts
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Assay Systems
Formal Languages and Automata Theory
Models of Computation
Register-Transfer-Level Implementation
Software Testing
Control Structures and Microprogramming
Temporal Logic in Multi-Agent Systems
References
Alur R., Dill D.: A theory of timed automata. Theor. Comput. Sci.
126
, 183–235 (1994)
Article
MATH
MathSciNet
Google Scholar
Baeten J.C.M., Middelburg C.A.: Process Algebra with Timing EATCS. Monograph. Springer, Berlin (2002)
Google Scholar
Barnard J.: COMX: a design methodology using communicating X-machines. Inform. Softw. Technol.
40
(5–6), 271–280 (1998)
Article
Google Scholar
Batth, S.S., Rodrigues Vieira, E., Cavalli, A., Uyar, M.Ü.: Specification of timed EFSM fault models in SDL. In: 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE’07. Lecture Notes in Computer Sciences, vol. 4574, pp. 50–65. Springer, Berlin (2007)
Bogdanov K., Holcombe M., Ipate F., Seed L., Vanak S.: Testing methods for X-machines: a review. Formal Asp. Comput.
18
, 3–30 (2006)
Article
MATH
Google Scholar
Bosik B.S., Uyar M.Ü.: Finite state machine based formal methods in protocol conformance testing. Comput. Netw. ISDN Syst.
22
, 7–33 (1991)
Article
Google Scholar
Brandán Briones, L., Brinksma, E.: Testing real-time multi input-output systems. In: 7th International Conference on Formal Engineering Methods, ICFEM’05. Lecture Notes in Computer Sciences, vol. 3785, pp. 264–279. Springer, Berlin (2005)
Brinksma, E., Tretmans, J.: Testing transition systems: an annotated bibliography. In: 4th Summer School on Modeling and Verification of Parallel Processes, MOVEP’00. Lecture Notes in Computer Sciences, vol. 2067, pp. 187–195. Springer, Berlin (2001)
Cardell-Oliver R.: Conformance tests for real-time systems with timed automata specifications. Formal Asp. Comput.
12
(5), 350–371 (2000)
Article
MATH
Google Scholar
Cardell-Oliver, R., Glover, T.: A practical and complete algorithm for testing real-time systems. In: 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT’98. Lecture Notes in Computer Sciences, vol. 1486, pp. 251–260. Springer, Berlin (1998)
Chow T.S.: Testing software design modelled by finite state machines. IEEE Trans. Softw. Eng.
, 178–187 (1978)
Article
Google Scholar
Clarke, D., Lee, I.: Automatic generation of tests for timing constraints from requirements. In: 3rd Workshop on Object-Oriented Real-Time Dependable Systems, WORDS’97, pp. 199–206. IEEE Computer Society Press, New York (1997)
Davies J., Schneider S.: A brief history of timed CSP. Theor. Comput. Sci.
138
, 243–271 (1995)
Article
MATH
MathSciNet
Google Scholar
El-Fakih K., Yevtushenko N., von Bochmann G.: FSM-based incremental conformance testing methods. IEEE Trans. Softw. Eng.
30
(7), 425–436 (2004)
Article
Google Scholar
En-Nouaary A., Dssouli R., Khendek F.: Timed Wp-method: testing real time systems. IEEE Trans. Softw. Eng.
28
(11), 1024–1039 (2002)
Article
Google Scholar
Fouchal, H., Petitjean, E., Salva, S.: An user-oriented testing of real time systems. In: IEEE Workshop on Real-Time Embedded Systems, RTES’01. IEEE Computer Society Press, New York (2001)
Hennessy M., Regan T.: A process algebra for timed systems. Inform. Comput.
117
(2), 221–239 (1995)
Article
MATH
MathSciNet
Google Scholar
Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Formal Methods and Testing. Lecture Notes in Computer Sciences, vol. 4949, pp. 77–117. Springer, Berlin (2008)
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 methods to support testing. ACM Comput. Surv.
41
(2) (2009)
Hierons, R.M., Bowen, J.P., Harman, M. (eds): Formal Methods and Testing. Lecture Notes in Computer Sciences, vol. 4949. Springer, Berlin (2008)
Google Scholar
Hierons R.M., Harman M.: Testing conformance of a deterministic implementation to a non-deterministic stream X-machine. Theor. Comput. Sci.
323
(1–3), 191–233 (2004)
Article
MATH
MathSciNet
Google Scholar
Hierons R.M., Ipate F.: Testing a deterministic implementation against a non-controllable non-deterministic stream X-machine. Formal Asp. Comput.
20
(6), 597–617 (2008)
Article
MATH
Google Scholar
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)
Article
MATH
Google Scholar
Higashino, T, Nakata, A, Taniguchi, K., Cavalli, A.: Generating test cases for a timed I/O automaton model. In: 12th International Workshop on Testing of Communicating Systems, IWTCS’99, pp. 197–214. Kluwer, Dordrecht (1999)
Holcombe M., Ipate F.: Correct Systems: Building a Business Process Solution. Springer, Berlin (1998)
MATH
Google Scholar
Ipate F.: Testing against a non-controllable stream X-machine using state counting. Theor. Comput. Sci.
353
(1), 291–316 (2006)
Article
MATH
MathSciNet
Google Scholar
Ipate F., Holcombe M.: An integration testing method that is proved to find all faults. Int. J. Comput. Math.
63
(3–4), 159–178 (1997)
Article
MATH
MathSciNet
Google Scholar
Ipate F., Holcombe M.: Testing data processing-oriented systems from Stream X-machine models. Theor. Comput. Sci.
403
(2–3), 171–191 (2008)
MathSciNet
Google Scholar
Kefalas P., Eleftherakis G., Kehris E.: Communicating X-machines: a practical approach for formal and modular specification of large systems. Inform. Softw. Technol.
45
(5), 269–280 (2003)
Article
Google Scholar
Kehris E., Eleftherakis G., Kefalas P.: Using X–machines to model and test discrete event simulation programs. In: Mastorakis, N. (eds) Systems and Control: Theory and Applications, pp. 163–171. World Scientific and Engineering Society Press, Greece (2000)
Google Scholar
Krichen, M., Tripakis, S.: An expressive and implementable formal framework for testing real-time systems. In: 17th International Conference on Testing of Communicating Systems, TestCom’05. Lecture Notes in Computer Sciences, vol. 3502, pp. 209–225. Springer, Berlin (2005)
Lee D., Yannakakis M.: Principles and methods of testing finite state machines: a survey. Proc. IEEE
84
(8), 1090–1123 (1996)
Article
Google Scholar
Mandrioli D., Morasca S., Morzenti A.: Generating test cases for real time systems from logic specifications. ACM Trans. Comput. Syst.
13
(4), 356–398 (1995)
Article
Google Scholar
Merayo, M.G., Hierons, R.M., Núñez, M.: Extending stream X-machines to specify and test systems with timeouts. In: 6th IEEE International Conference on Software Engineering and Formal Methods, SEFM’08, pp. 201–210. IEEE Computer Society Press, New York (2008)
Merayo, M.G., Núñez, M.: Testing conformance on stochastic stream X-machines. In: 5th IEEE International Conference on Software Engineering and Formal Methods, SEFM’07, pp. 227–236. IEEE Computer Society Press, New York (2007)
Merayo M.G., Núñez M., Rodríguez I.: Extending EFSMs to specify and test timed systems with action durations and timeouts. IEEE Trans. Comput.
57
(6), 835–848 (2008)
Article
MathSciNet
Google Scholar
Merayo M.G., Núñez M., Rodríguez I.: Formal testing from timed finite state machines. Comput. Netw.
52
(2), 432–460 (2008)
Article
MATH
Google Scholar
Nicollin, X., Sifakis, J.: An overview and synthesis on timed process algebras. In: 3rd International Conference on Computer Aided Verification, CAV’91. Lecture Notes in Computer Sciences, vol. 575, pp. 376–398. Springer, Berlin (1991)
Peleska J., Siegel M.: Test automation of safety-critical reactive systems. S. Afr. Comput. J.
19
, 53–77 (1997)
Google Scholar
Petrenko, A.: Fault model-driven test derivation from finite state models: annotated bibliography. In: 4th Summer School on Modeling and Verification of Parallel Processes, MOVEP’00. Lecture Notes in Computer Sciences, vol. 2067, pp. 196–205. Springer, Berlin (2001)
Petrenko, A., Yevtushenko, N., von Bochmann, G.: Testing deterministic implementations from their nondeterministic FSM specifications. In: 9th IFIP Workshop on Testing of Communicating Systems, IWTCS’96, pp. 125–140. Chapman & Hall, London (1996)
Petrenko, A., Yevtushenko, N., Lebedev, A.V., Das, A.: Nondeterministic state machines in protocol conformance testing. In: 6th IFIP Workshop on Protocol Test Systems, IWPTS’93, pp. 363–378. North-Holland, Amsterdam (1993)
Quemada J., de Frutos D., Azcorra A.: TIC: a timed calculus. Formal Asp. Comput.
, 224–252 (1993)
Article
MATH
Google Scholar
Reed G.M., Roscoe A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci.
58
, 249–261 (1988)
Article
MATH
MathSciNet
Google Scholar
Rodríguez I., Merayo M.G., Núñez M.:
\({\mathcal {HOT\,L}}\)
: hypotheses and observations testing logic. J. Log. Algebraic Program.
74
(2), 57–93 (2008)
Article
MATH
Google Scholar
Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’08. Lecture Notes in Computer Sciences, vol. 5215, pp. 250–264. Springer, Berlin (2008)
Sifakis, J.: Use of Petri nets for performance evaluation. In: 3rd International Symposium on Measuring, Modelling and Evaluating Computer Systems, pp. 75–93. North-Holland, Amsterdam (1977)
Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing timed automata. Theor. Comput. Sci.
254
(1–2), 225–257 (2001) [Previously appeared as Technical Report CTIT-97-17, University of Twente (1997)]
Google Scholar
Stannett, M.: Computation over arbitrary models of time. Technical Report CS-2001-08, Department of Computer Science, Sheffield University (2001)
Tretmans, J.: Model based testing with labelled transition systems. In: Formal Methods and Testing. Lecture Notes in Computer Sciences, vol. 4949, pp. 1–38. Springer, Berlin (2008)
Uyar M.Ü., Batth S.S., Wang Y., Fecko M.A.: Algorithms for modeling a class of single timing faults in communication protocols. IEEE Trans. Comput.
57
(2), 274–288 (2008)
Article
Google Scholar
Uyar M.Ü., Fecko M.A., Sethi A.S., Amar P.D.: Testing protocols modeled as FSMs with timing parameters. Comput. Netw.
31
(18), 1967–1998 (1999)
Article
Google Scholar
Yi, W.: CCS+ Time = an interleaving model for real time systems. In: 18th International Colloquium on Automata, Languages and Programming, ICALP’91. Lecture Notes in Computer Sciences, vol. 510, pp. 217–228. Springer, Berlin (1991)
Download references
Author information
Authors and Affiliations
Dep. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, 28040, Madrid, Spain
Mercedes G. Merayo & Manuel Núñez
School of Information Systems and Computing Mathematics, Brunel University, Uxbridge, Middlesex, UB8 3PH, UK
Robert M. Hierons
Authors
Mercedes G. Merayo
View author publications
Search author on:
PubMed
Google Scholar
Manuel Núñez
View author publications
Search author on:
PubMed
Google Scholar
Robert M. Hierons
View author publications
Search author on:
PubMed
Google Scholar
Corresponding author
Correspondence to
Mercedes G. Merayo
Additional information
Communicated by Dr. Antonio Cerone.
This paper represents an extended and improved version of [34]. This research was partially supported by the Spanish MEC project WEST/FAST (TIN2006-15578-C02-01).
Rights and permissions
Reprints and permissions
About this article
Cite this article
Merayo, M.G., Núñez, M. & Hierons, R.M. Testing timed systems modeled by Stream X-machines.
Softw Syst Model
10
, 201–217 (2011). https://doi.org/10.1007/s10270-009-0126-3
Download citation
Received
02 March 2009
Revised
15 July 2009
Accepted
23 July 2009
Published
14 August 2009
Issue date
May 2011
DOI
Share this article
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Formal testing
Timed systems
Stream X-machines
Profiles
Mercedes G. Merayo
View author profile
Access this article
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Price includes VAT (France)
Instant access to the full article PDF.
Institutional subscriptions
Advertisement