Abstract
The Connect project aims to enable the seamless composition of heterogeneous networked systems. In this context, Verification and Validation (V&V) techniques are sought to ensure that the Connected system satisfies dependability requirements. Stochastic model checking and state-based stochastic methods are two appealing V&V approaches to accomplish this task. In this paper, we report on the application of the two approaches in a typical Connect scenario. Specifically, we make clear (i) how the two approaches can be employed to enhance the confidence in the correctness of the analysis, and (ii) how the complementarity of these approaches can be fruitfully exploited to extend the analysis.
This work is supported by the European FP 7 project CONNECT (IST 231167).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avizienis, A., Laprie, J.-C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Transactions on Dependable and Secure Computing 1(1), 11–33 (2004)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–161. Springer, Heidelberg (1999)
Bertolino, A., Di Giandomenico, F., Di Marco, A., Issarny, V., Martinelli, F., Masci, P., Matteucci, I., Saadi, R., Sabetta, A.: Dependability in dynamic, evolving and heterogeneous systems: the connect approach. In: Proc. 2nd International Workshop on Software Engineering for Resilient Systems, SERENE2010 (2010)
Bertolino, A., Inverardi, P., Issarny, V., Sabetta, A., Spalazzese, R.: On-the-fly interoperability though automated mediator synthesis and monitoring. In: ISoLA 2010, Part II. LNCS, vol. 6416, pp. 251–262. Springer, Heidelberg (2010)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026. Springer, Heidelberg (1995)
Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic QoS management and optimisation in service-based systems. IEEE Transaction on Software Engineering (to appear)
Clark, G., Courtney, T., Daly, D., Deavours, D.D., Derisavi, S., Doyle, J.M., Sanders, W.H., Webster, P.G.: The Möbius modeling tool. In: 9th Int. Workshop on Petri Nets and Performance Models, pp. 241–250. Aachen, Germany, Los Alamitos (September 2001)
Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proc. 7th International Conference on Quantitative Evaluation of Systems (QEST 2010). IEEE CS Press, Los Alamitos (2010)
Gulati, R., Dugan, J.B.: A modular approach for analyzing static and dynamic fault trees. In: Annual Reliability and Maintainability Symposium, pp. 57–63. IEEE Computer Society Press, Los Alamitos (1997)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, Springer, Heidelberg (2006)
Inverardi, P., Issarny, V., Spalazzese, R.: A theory of mediators for eternal connectors. In: ISoLA 2010, Part II, 2010. LNCS, vol. 6416, pp. 236–250. Springer, Heidelberg (2010)
Issarny, V., Steffen, B., Jonsson, B., Blair, G., Grace, P., Kwiatkowska, M., Calinescu, R., Inverardi, P., Tivoli, M., Bertolino, A., Sabetta, A.: Connect Challenges: Towards Emergent connectors for Eternal Networked Systems. In: 14th IEEE International Conference on Engineering of Complex Computer Systems, pp. 154–161. IEEE Computer Society, Los Alamitos (2009)
Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 6015, pp. 23–37. Springer, Heidelberg (2010)
Leland, W.E., Taqqu, M.S., Willinger, W., Wilson, D.V.: On the self-similar nature of ethernet traffic (extended version). IEEE/ACM Transactions on Networking 2(1), 1–15 (1994)
Masci, P., Chiaradonna, S., Di Giandomenico, F.: Dependability analysis of diffusion protocols in wireless networks with heterogeneous node capabilities. In: 8th European Dependable Computing Conference (EDCC2010), pp. 145–154. IEEE Computer Society, Los Alamitos (2010)
Nicol, D.M., Sanders, W.H., Trivedi, K.S.: Model-based evaluation: from dependability to security. IEEE Transactions on Dependable and Secure Computing 1, 48–65 (2004)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)
Sanders, W.H., Meyer, J.F.: Stochastic Activity Networks: formal definitions and concepts, pp. 315–343 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Giandomenico, F., Kwiatkowska, M., Martinucci, M., Masci, P., Qu, H. (2010). Dependability Analysis and Verification for Connected Systems. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16561-0_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-16561-0_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16560-3
Online ISBN: 978-3-642-16561-0
eBook Packages: Computer ScienceComputer Science (R0)