caa a22 4500 605516243 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20151101xx s 000 0 eng 10.1007/s00165-014-0331-x doi (NATIONALLICENCE)springer-10.1007/s00165-014-0331-x Model checking the observational determinism security property using PROMELA and SPIN [Elektronische Daten] [Maryam Dabaghchian, Mohammad Abdollahi Azgomi] Observational determinism is a property that ensures the confidentiality in concurrent programs. It conveys that public variables are independent of private variables during the execution of programs, and the scheduling policy of threads. Different definitions for observational determinism have been proposed. On the other hand, observational determinism is not a standard property and it should be checked over two or more executions of a program. The self-composition approach allows comparing two different copies of a program using a single formula. In this paper, we propose a new specification for the observational determinism security property in linear temporal logic. We also present a general method to create the appropriate program model using the self-composition approach. Both the program model and the observational determinism property are encoded in embedded C codes in PROMELA using the SPIN model checker. The paper also discusses a method for the instrumentation of PROMELA code in order to encode the program model for specifying the observational determinism security property. British Computer Society, 2015 Model checking nationallicence Linear temporal logic (LTL) nationallicence Information flow security nationallicence Observational determinism nationallicence SPIN nationallicence PROMELA nationallicence Dabaghchian Maryam Department of Computer Engineering, Science and Research Branch, Islamic Azad University, Tehran, Iran aut Abdollahi Azgomi Mohammad Trsutworthy Computing Laboratory, School of Computer Engineering, Iran University of Science and Technology, Hengam St., Resalat Sq., Tehran, Iran aut Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 789-804 0934-5043 27:5-6<789 2015 27 165 https://doi.org/10.1007/s00165-014-0331-x text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0331-x text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Dabaghchian Maryam Department of Computer Engineering, Science and Research Branch, Islamic Azad University, Tehran, Iran aut NATIONALLICENCE 700 1- Abdollahi Azgomi Mohammad Trsutworthy Computing Laboratory, School of Computer Engineering, Iran University of Science and Technology, Hengam St., Resalat Sq., Tehran, Iran aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 789-804 0934-5043 27:5-6<789 2015 27 165