Abstract
In the present paper we assess both the safety properties and the response-time profile of a subscription service which provides medical assistance to drivers who are injured in vehicular collisions. We use both timed and untimed process calculi cooperatively to perform the required analysis. The formal analysis tools used are hosted on a high-level modelling platform with support for scripting and orchestration which enables users to build custom analysis processes from the general-purpose analysers which are hosted as services on the platform.
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
Magee, J., Kramer, J.: Concurrency - State Models and Java Programs, 2nd edn. John Wiley, Chichester (2006)
Magee, J., Kramer, J., Giannakopoulou, D.: Analysing the behaviour of distributed software architectures: a case study. In: 5th IEEE Workshop on Future Trends of Distributed Computing Systems, Tunisia (1997)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Tribastone, M.: The PEPA Plug-in Project. In: Harchol-Balter, M., Kwiatkowska, M., Telek, M. (eds.) Proceedings of the 4th International Conference on the Quantitative Evaluation of SysTems (QEST), pp. 53–54. IEEE Computer Society Press, Los Alamitos (2007)
Clark, A.: The ipclib PEPA Library. In: Harchol-Balter, M., Kwiatkowska, M., Telek, M. (eds.) Proceedings of the 4th International Conference on the Quantitative Evaluation of SysTems (QEST), pp. 55–56. IEEE Computer Society Press, Los Alamitos (2007)
Grassmann, W.: Transient solutions in Markovian queueing systems. Computers and Operations Research 4, 47–53 (1977)
Gross, D., Miller, D.: The randomization technique as a modelling tool and solution procedure for transient Markov processes. Operations Research 32, 343–361 (1984)
Argent-Katwala, A., Bradley, J., Dingle, N.: Expressing performance requirements using regular expressions to specify stochastic probes over process algebra models. In: Proceedings of the Fourth International Workshop on Software and Performance, Redwood Shores, California, USA, pp. 49–58. ACM Press, New York (2004)
Clark, A., Gilmore, S.: Evaluating quality of service for service level agreements. In: Brim, L., Leucker, M. (eds.) Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems, Bonn, Germany, pp. 172–185 (2006)
ter Beek, M.H., Gnesi, S., Koch, N., Mazzanti, F.: Formal verification of an automotive scenario in service-oriented computing. In: Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, pp. 613–622. ACM Press, New York (2008)
UMC model checker (2008), http://fmt.isti.cnr.it/umc/
Lapadula, A., Pugliese, R., Tiezzi, F.: Specifying and analysing SOC applications with COWS. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 701–720. Springer, Heidelberg (2008)
Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based Verification of Web Service Compositions. In: Proc. of the 18th IEEE Int. Conference on Automated Software Engineering, pp. 152–161. IEEE Computer Society Press, Los Alamitos (2003)
Foster, H., Emmerich, W., Magee, J., Kramer, J., Rosenblum, D., Uchitel, S.: Model Checking Service Compositions under Resource Constraints. In: The European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007) (2007)
Badica, C., Badica, A., Litoiu, V.: Role activity diagrams as finite state processes. In: Second International Symposium on Parallel and Distributed Computing (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Argent-Katwala, A., Clark, A., Foster, H., Gilmore, S., Mayer, P., Tribastone, M. (2008). Safety and Response-Time Analysis of an Automotive Accident Assistance Service. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. ISoLA 2008. Communications in Computer and Information Science, vol 17. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88479-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-88479-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88478-1
Online ISBN: 978-3-540-88479-8
eBook Packages: Computer ScienceComputer Science (R0)