Abstract
We present a tool for analysing resource sharing conflicts in multithreaded Java programs. Java programs are translated to timed automata models verified afterwards by the Uppaal model checker. Analysed programs are annotated with timing information indicating the execution duration of a particular statement. Based on the timing information, the analysis of execution paths is performed, which gives an answer whether resource sharing conflicts are possible in a multithreaded Java program. If the analysis succeeds, resource locks may be eliminated from the Java program.
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.
References
Baklanova, N., Strecker, M., Féraud, L.: Resource sharing conflicts checking in multithreaded Java programs. In: Journées FAC 2012 (2012)
Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354, 301–317 (2006)
Bøgholm, T., Kragh-Hansen, H., Olsen, P.: Model based schedulability analysis of real-time systems. Master’s thesis, Aalborg University (2008)
Bøgholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time Java programs. In: Bollella, G., Locke, C.D. (eds.) JTRES. ACM International Conference Proceeding Series, vol. 343, pp. 106–114. ACM (2008)
Hakimipour, N., Strooper, P., Wellings, A.: A model-based development approach for the verification of real-time java code. Concurrency and Computation: Practice and Experience 23(13), 1583–1606 (2011)
Herber, P., Pockrandt, M., Glesner, S.: Transforming systemc transaction level models into uppaal timed automata. In: 2011 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 161–170 (2011)
Cordovilla, M., Boniol, F., Noulard, E., Pagetti, C.: Multiprocessor schedulability analyser. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.C. (eds.) SAC, pp. 735–741. ACM (2011)
Ravn, A.P., Schoeberl, M.: Cyclic executive for safety-critical java on chip-multiprocessors. In: Kalibera, T., Vitek, J. (eds.) JTRES. ACM International Conference Proceeding Series, pp. 63–69. ACM (2010)
Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic Verification of Determinism for Structured Parallel Programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455–471. Springer, Heidelberg (2010)
Tofan, B., Schellhorn, G., Bäumler, S., Reif, W.: Embedding rely-guarantee reasoning in temporal logic. Technical Report 2010-07, Informatik (2010)
The Real-Time for Java Expert Group: The Real-Time Specification for Java (2006)
The Open Group JSR: JSR-302 Safety Critical Java Technology Specification (2010), http://jcp.org/en/jsr/detail?id=308
Henties, T., Hunt, J.J., Locke, D., Nilsen, K., Schoeberl, M., Vitek, J.: Java for safety-critical applications. In: 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems, SafeCert 2009 (March 2009)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004), http://dx.doi.org/10.1007/978-3-540-27755-2_3
Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 414–425 (June 1990)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: a time-triggered language for embedded programming. Proceedings of the IEEE 91(1), 84–99 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baklanova, N., Strecker, M. (2013). Abstraction and Verification of Properties of a Real-Time Java. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds) ICT in Education, Research, and Industrial Applications. ICTERI 2012. Communications in Computer and Information Science, vol 347. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35737-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-35737-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35736-7
Online ISBN: 978-3-642-35737-4
eBook Packages: Computer ScienceComputer Science (R0)