Statistical abstraction and model-checking of large heterogeneous systems

被引：24

作者：

Basu A. ^{[1
]}

Bensalem S. ^{[1
]}

Bozga M. ^{[1
]}

Delahaye B. ^{[2
]}

Legay A. ^{[3
]}

机构：

[1] Verimag Laboratory, Université Joseph Fourier, CNRS, Grenoble

[2] Université de Rennes 1/IRISA, Rennes

[3] INRIA/IRISA, Rennes

来源：

International Journal on Software Tools for Technology Transfer | 2012年 / 14卷 / 01期

关键词：

Heterogeneous systems; Simulation; Statistical model checking; Stochastic abstraction;

D O I：

10.1007/s10009-011-0201-2

中图分类号：

学科分类号：

摘要：

We propose a new simulation-based technique for verifying applications running within a large heterogeneous system. Our technique starts by performing simulations of the system to learn the context in which the application is used. Then, it creates a stochastic abstraction for the application, which considers the context information. This smaller model can be verified using efficient techniques such as statistical model checking. We have applied our technique to an industrial case study: the cabin communication system of an airplane. We use the BIP toolset to model and simulate the system. We have conducted experiments to verify the clock synchronization protocol i. e., the application used to synchronize the clocks of all computing devices within the system. © 2011 Springer-Verlag.

引用

页码：53 / 72

页数：19

共 33 条

[1]

Aircraft Data Network, (2005)

[2]

II61588: Precision clock synchronization protocol for networked measurement and control systems, (2004)

[3]

Alur R., Dill D., A theory of timed automata, Theor. Comput. Sci., 126, pp. 183-235, (1994)

[4]

Basu A., Bensalem S., Bozga M., Delahaye B., Legay A., Siffakis E., Verification of an afdx infrastructure using simulations and probabilities, In: Proceedings of 1st Conference on Runtime Verification (RV), (2010)

[5]

Basu A., Bozga M., Sifakis J., Modeling heterogeneous real-time systems in BIP, In: SEFM06, pp. 3-12, (2006)

[6]

Basu A., Bensalem S., Bozga M., Caillaud B., Delahaye B., Legay A., Statistical abstraction and model-checking of large heterogeneous systems, In: FORTE 2010, pp. 32-48, (2010)

[7]

Bensalem S., Delahaye B., Legay A., Statistical model checking: present and future, In: Proceedings of 1st Conference on Runtime Verification (RV), (2010)

[8]

Bucklew J., Introduction to Rare Event Simulation, (2004)

[9]

Charara H., Fraboul C., Modelling and simulation of an avionics full duplex switched ethernet, (2005)

[10]

Charara H., Scharbarg J.L., Ermont J., Fraboul C., Methods for bounding end-to-end delays on AFDX network, In: ECRTS, (2006)

← 1 2 3 4 →