Abstract
Traditional testing techniques often reach their limits when employed for the assessment of critical Machine Control Systems as they contain a large amount of random and unpredictable components. The probabilistic analysis approach can assist in their evaluation by providing a subjective evidence of their safety and reliability. The synergy of probabilistic analysis and expressiveness of higher-order logic theorem proving results into convincing modelling and reasoning of several stringent safety cases that contribute towards the certification of high-assurance systems.
Chapter PDF
Similar content being viewed by others
Keywords
- Model Check
- Probabilistic Analysis
- Discrete Random Variable
- Continuous Random Variable
- Unmanned Aerial System
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Dźwiarek, M.: An analysis of accidents caused by improper functioning of machine control systems. International Journal of Occupational Safety and Ergonomics 10(2), 129–136 (2004)
Heinrich, H.: Industrial Accident Prevention: A Scientific Approach. McGraw Hill Inc. (1941)
Bishop, P., Bloomfield, R.: A methodology for safety case development. In: Safety-Critical System Symposium, Birmingham, UK. Springer (1998)
Mashkoor, A., Jacquot, J.-P.: Stepwise validation of formal specifications. In: 18th Asia-Pacific Software Engineering Conference (APSEC 2011), Ho Chi Minh City, Vietnam. IEEE (2011)
Yang, F., Jacquot, J.-P.: Scaling up with Event-B: A case study. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 438–452. Springer, Heidelberg (2011)
Panesar-Walawege, R., Sabetzadeh, M., Briand, L., Coq, T.: Characterizing the chain of evidence for software safety cases: A conceptual model based on the IEC 61508 standard. In: 3rd International Conference on Software Testing, Verification and Validation (ICST 2010), pp. 335–344 (2010)
Fong, E., Kass, M., Rhodes, T., Boland, F.: Structured assurance case methodology for assessing software trustworthiness. In: 4th International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C 2010), pp. 32–33 (2010)
Graydon, P.J., Knight, J.C., Strunk, E.A.: Assurance-based development of critical systems. In: 37th International Conference on Dependable Systems and Networks (DSN 2007), pp. 347–357. IEEE, Washington, DC (2007)
Rushby, J.: A safety-case approach for certifying adaptive systems. In: AIAA Infotech@Aerospace Conference, American Institute of Aeronautics and Astronautics (2009)
Rushby, J.: Formalism in safety cases. In: Dale, C., Anderson, T. (eds.) 18th Safety-Critical Systems Symposium, Bristol, UK, pp. 3–17. Springer (2010)
Herencia-Zapana, H., Hagen, G., Narkawicz, A.: Formalizing probabilistic safety claims. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 162–176. Springer, Heidelberg (2011)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model Checking Algorithms for Continuous time Markov Chains. IEEE Transactions on Software Engineering 29(4), 524–541 (2003)
Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, vol. 23. American Mathematical Society (2004)
Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
Abrial, J.-R.: The B Book. Cambridge University Press (1996)
Abrial, J.-R.: Modelling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Hallerstede, S., Hoang, T.S.: Qualitative probabilistic modelling in Event-B. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 293–312. Springer, Heidelberg (2007)
Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Towards probabilistic modelling in Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 275–289. Springer, Heidelberg (2010)
Hurd, J.: Formal verification of probabilistic algorithms. PhD Thesis, University of Cambridge, Cambridge, UK (2002)
Mhamdi, T., Hasan, O., Tahar, S.: Formalization of Entropy Measures in HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 233–248. Springer, Heidelberg (2011)
Hölzl, J., Heller, A.: Three Chapters of Measure Theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135–151. Springer, Heidelberg (2011)
Hasan, O., Tahar, S.: Formal Probabilistic Analysis: A Higher-order Logic based approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 2–19. Springer, Heidelberg (2010)
Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940)
Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 348–375 (1977)
Mashkoor, A., Hasan, O.: Formal probabilistic analysis of cyber-physical transportation systems. In: Murgante, B., Gervasi, O., Misra, S., Nedjah, N., Rocha, A.M.A.C., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2012, Part III. LNCS, vol. 7335, pp. 419–434. Springer, Heidelberg (2012)
Hasan, O., Tahar, S.: Using theorem proving to verify expectation and variance for discrete random variables. J. Autom. Reasoning 41(3-4), 295–323 (2008)
Harrison, J.: Theorem Proving with the Real Numbers. Springer (1998)
Parker, L.E.: Multiple mobile robot teams, path planning and motion coordination. In: Encyclopedia of Complexity and Systems Science, pp. 5783–5800. Springer (2009)
Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)
Sen, K., Viswanathan, M., Agha, G.: Vesta: A statistical model-checker and analyzer for probabilistic systems. In: Second International Conference on the Quantitative Evaluation of Systems, pp. 251–252 (September 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Mashkoor, A., Hasan, O., Beer, W. (2013). Using Probabilistic Analysis for the Certification of Machine Control Systems. In: Cuzzocrea, A., Kittl, C., Simos, D.E., Weippl, E., Xu, L. (eds) Security Engineering and Intelligence Informatics. CD-ARES 2013. Lecture Notes in Computer Science, vol 8128. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40588-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-40588-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40587-7
Online ISBN: 978-3-642-40588-4
eBook Packages: Computer ScienceComputer Science (R0)