李枫+OS2ATC2026__SPARK+in+Kernel+Development__FengLi-20260328p+2026-4-1+214937+1.pdf

1、 in Kernel Developmentin Kernel Development Feng Li(李枫李枫) Mar 28,2026 An indie developer from China：The main translator of the book Gray Hat Hacking The Ethical Hackers Handbook,Fourth Edition (ISBN：9787302428671)&Linux Hardening in Hostile Networks,First Edition (ISBN:9787115544384)Pure software de

2、velopment for 15 years (11 years on Mobile dev)Actively participating Open Source Communities:https:/ https:/ Recently,focus on infrastructure of Cloud/Edge Computing,AI,IoT,OS,Programming Languages&Runtimes,Network,Virtualization,RISC-V,EDA,5G/6G Who Am I Agenda I.Background An overview of Ada/SPAR

3、K Testbeds Practices II.Ironclad Overview Practices III.HiRTOS Overview Running on Renode IV.The Return of Ada?Ranking Ecosystem HW-SW Co-design V.Wrap-up 1)An Overview of Ada/SPARK 1.1 Ada I.Background https:/en.wikipedia.org/wiki/Ada_(programming_language)I.Background I.Background Source:https:/en

4、.wikipedia.org/wiki/List_of_compilers#Ada_compilers 1.2 SPARK I.Background https:/en.wikipedia.org/wiki/SPARK_(programming_language)I.Background I.Background Key advantages https:/ I.Background I.Background 1.2.1 Src https:/ I.Background 1.2.1.1 Why3 https:/ I.Background 1.2.1.2 SPARKlib https:/ I.B

5、ackground 1.2.2 Comparison.I.Background Source:https:/ Source:https:/ 1.2.3 Development https:/ https:/ https:/ https:/ I.Background 1.2.3.1 Alire https:/ 1.2.3.2 Renode https:/renode.io/A lightweight virtual development framework with an IoT focus.I.Background Supported boards https:/renode.readthe

6、docs.io/en/latest/introduction/supported-boards.html For more details,you may refer to our previous talk Revisiting Renode as a Swiss Army Knife for RISC-V development at COSCon 2024 and the follow-ups.Src&binaries https:/ I.Background Source:https:/ Source:https:/ 2)Testbeds 2.1 Testbed1(GMK K8 PLU