Training Materials

• Introduction to the POK project
• Specify system requirements (either by AADL or XML files)
• Code Generation patterns used by Ocarina to generate code that targets POK Operating System
• Validation and Certification tools for POK
• Overview of the POK Operating System

Technical Materials

• Build PowerPC toolchain
• Build Leon toolchain

Academic publications

• Delange, Julien, et al. “An Architecture-Centric Process for MILS Development.”
• J. Delange and Laurent Lec. POK, an ARINC653-compliant operating system released under the BSD license. In - 13th Real-Time Linux Workshop.
• J. Delange, L. Pautet, Alain Plantec, Mickael Kerboeuf, Frank Singhoff and Fabrice Kordon. Validate, simulate and implement ARINC653 systems using the AADL. In ACM’s 12th Annual International Conference on Ada and Related Technologies - SIGAda09
• J. Delange, O. Gilles, J. Hugues and L. Pautet. Model-Based Engineering for the Development of Partitioned Architectures In AeroTech Congress & Exhibition - Avionics - Integrated Model-based System, Application and Architectures.
• J. Delange, L. Pautet and Peter Feiler. Validating safety and security requirements for partitioned architectures. In 14th International Conference on Reliable Software Technologies - Ada Europe, June 2009.
• J. Delange, L. Pautet and F. Kordon. Code Generation Strategies for Partitioned Systems. In 29th IEEE Real-Time Systems Symposium (RTSS’08) Work In Progress, IEEE Computer Society, December 2008.

Related publications

• Design and architecture of real-time operating system
• Zhao, Yongwang, et al. “Reasoning about information flow security of separation kernels with channel-based communication.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2016.
• Zhao, Yongwang, Zhibin Yang, and Dianfu Ma. “A survey on formal specification and verification of separation kernels.” Frontiers of Computer Science 11.4 (2017): 585-607.
• Zhao, Yongwang, et al. “Refinement-based Specification and Security Analysis of Separation Kernels.” IEEE Transactions on Dependable and Secure Computing (2017).
• Zhao, Yongwang, et al. “High-Assurance Separation Kernels: A Survey on Formal Methods.” arXiv preprint arXiv:1701.01535 (2017).
• Zhao, Yongwang. “Formal specification and verification of separation kernels: An overview.” ArXiv e-prints, no (2015).
• Carvalho, Adriano, et al. “Functionality Farming in POK/Rodosvisor.”