Formal Architecture Based Design Analysis for Certifying SWS RTOS

In recent times Formal Techniques have been strongly recommended in the engineering life-cycle of safety -critical systems. With this, Architecture Analysis & Design Language (AADL) is a widely spectrum accepted architecture modeling language that can be wrap with Formal Modeling techniques, that proficiently helps in the design of a safety-critical system and circumscribes various analytical features for modeling the hardware and software architecture/s, against the required as per the guidelines set aside in RTCA DO-178C (333- Formal Based Modeling). This paper discusses the use of architecture modeling language along with formal based techniques for the analysis of RTOS architecture which is important in the correct implement of the given requirements. The architecture of the RTOS is expressed and analyzed using AADL. A suitable case study such as Stall Warning System/Aircraft Interface Computer (SWS/AIC), RTOS scheduler is modeled and analyzed. The analysis of results are mapped to the workflow prescribed in RTCA DO-178C for generating the certificate artifact and establishing the effectiveness of architecture based design analysis in the software engineering process.