@TechReport{ hoang.ea:specifying:2009, abstract = {We investigate the idea of developing access control systemsin Event-B by specifying separately the \"insecure\" target system andthe security authorisation, then combining them together in order toconstruct a secure system. This is based on the work by Basin et. al. [6]where the chosen language is CSP-OZ. Moreover, in order to verify thesecure system against some safety temporal properties, we propose anapproach of constructing several abstract models corresponding to theseproperties, and using refinement to prove that the final system satisfiesthese properties.}, author = {Thai Son Hoang and David Basin and Jean-Raymond Abrial}, institution = {Department of Computer Science, ETH Zurich}, language = {USenglish}, month = 6, number = 624, title = {Specifying Access Control in Event-B}, year = 2009, user = {htson} }