This is an Event-B model and Proofs of ARINC 653 Part 1 - 3 (2010). During modeling and verification, we found 6 safety errors in the ARINC 653 standard. These errors have been confirmed by the standard committee. For more information, please see our paper: Yongwang Zhao, Zhibin Yang, David Sanan, Yang Liu, "Event-based Formalization of Safety-critical Operating System Standards", 26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015) , November 2–5, 2015, Washington DC, USA.
The directory "ARINC653P1-3(2010)_Model2" is the project files in Rodin 3.2 (with Camille Editor plugin), which contains the event-b model files and all proofs.
For convenience, please see the PDF version of event-b sources using a Rodin Plugin - Camille Text Editor under the "PDF" directory.
Created by Yongwang Zhao (zhaoyongwang@gmail.com, zhaoyw@buaa.edu.cn), National Laboratory of Software Development Environment (NLSDE), School of Computer Science & Engineering, BeiHang Unversity (BUAA), Beijing, P.R.China