A measurable refinement method of design and verification for micro-kernel operating systems in communication network

Yang, 2021, Visual perception enabled industry intelligence: state of the art, challenges and prospects, IEEE Trans. Ind. Inf., 17, 2204, 10.1109/TII.2020.2998818 Yang, 2021, FADN: fully connected attitude detection network based on industrial video, IEEE Trans. Ind. Inf., 17, 2011, 10.1109/TII.2020.2984370 Yang, 2021, Robust six degrees of freedom estimation for IIoT based on multibranch network, IEEE Trans. Ind. Inf., 17, 2767, 10.1109/TII.2020.2982703 Jiang, 2021, Energy-efficient heterogeneous networking for electric vehicles networks in smart future cities, IEEE Trans. Intell. Transport. Syst., 22, 1868, 10.1109/TITS.2020.3029015 Yang, 2020, Fog-based marine environmental informationmonitoring towards ocean of things, IEEE Internet Things J., 7, 4238, 10.1109/JIOT.2019.2946269 Lv, 2021, Artificial intelligence for securing industrial-based cyber–physical systems, Future Generat. Comput. Syst., 117, 291, 10.1016/j.future.2020.12.001 Cao, 2020, Many-objective deployment optimization of edge devices for 5G networks, IEEE Trans. Netw. Sci. Eng., 7, 2117, 10.1109/TNSE.2020.3008381 Yang, 2020, Blockchain-based sharing and tamper-proof framework of big data networking, IEEE Netw, 34, 62, 10.1109/MNET.011.1900374 Wen, 2021, Big data driven marine environment information forecasting: a time series prediction network, IEEE Trans. Fuzzy Syst., 29, 4, 10.1109/TFUZZ.2020.3012393 Lv, 2021, Analysis of using blockchain to protect the privacy of drone big data, IEEE Netw, 35, 44, 10.1109/MNET.011.2000154 Li, 2005, Design of a servent based operating system, J. Comput. Res. Dev., 42, 1272, 10.1360/crad20050727 Liedtke, 1995, On micro-kernel construction, ACM SIGOPS - Oper. Syst. Rev., 29, 237, 10.1145/224057.224075 Shen, 2015, Microkernel mechanisms for improving the trustworthiness of commodity hardware, 155 Alkassar, 2009, Balancing the load: leveraging a semantics stack for systems verification, J. Autom. Reasoning, 42, 389, 10.1007/s10817-009-9123-z Zhou, 2005, Formal verification techniques in workflow process modeling, J. Comput. Res. Dev., 42, 1, 10.1360/crad20050101 Appel, 2016, Modular verification for computer security, 1 Walker, 1980, Specification and verification of the UCLA Unix security kernel, Commun. ACM, 23, 118, 10.1145/358818.358825 Gu, 2016, Certikos: an extensible architecture for building certified concurrent OS kernels, 653 Chen, 2018, Toward compositional verification of interruptible os kernels and device drivers, J. Autom. Reasoning, 61, 141, 10.1007/s10817-017-9446-0 Gu, 2019, Building certified concurrent OS kernels, Commun. ACM, 62, 89, 10.1145/3356903 Liu, 2020, Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation, 1 Xu, 2016, A practical verification framework for preemptive os kernels, 59 Ma, 2016, Formal verification of the message queue communication mechanism in μC/OS-II, Journal of Chinese Computer Systems, 37, 1179 Ding, 2018, End-to-end automated verification for OS kernels, 139 Elphinstone, 2013, From L3 to seL4 – what have we learnt in 20 years of L4 microkernels?, 133 Heiser, 2016, L4 microkernels: the lessons from 20 years of research and deployment, ACM Trans. Comput. Syst., 34, 1, 10.1145/2893177 Eldefrawy, 2017, Hydra: hybrid design for remote attestation (using a formally verified microkernel), 99 Ji, 2019, MicroTEE: designing TEE OS based on the microkernel architecture, 26 Klein, 2014, Comprehensive formal verification of an os microkernel, ACM Trans. Comput. Syst., 32, 10.1145/2560537 Klein, 2017, Provably trustworthy systems, Philosophical Transactions of the Royal Society A, 375, 1 Gu, 2019, Formalization and verification of several global properties of SpaceOS, Journal of Chinese Computer Systems, 40, 141 Liu, 2019, Multi-level reliable security mechanism based on spaceos, 1 Jiang, 2020, Operating system task management requirements layer modeling and verification based on Coq, J. Softw., 31, 2375 Liang, 2016, A correctness verification method for C programs based on VCC, 172 Ouyang, 2017, A safety-critical embedded real time operating system kernel design, Computer Engieering, 45, 78 Béchennec, 2018, Formal model-based conformance verification of an OSEK/VDX compliant RTOS, 628 Narayanan, 2019, Redleaf: towards an operating system for safe and verified firmware, 37 Zhang, 2020, Automatic kernel code synthesis and verification, Comput. Secur., 91, 101733, 10.1016/j.cose.2020.101733 Baumann, 2017, Compositional verification of security properties forembedded execution platforms, EPiC Series in Computing, 49, 1 Meng, 2019, Research on embedded dual operating system architecture based on trusted excution environmengt, Comput. Eng., 45, 6 Li, 2017, A distributed authentication and authorization scheme for in-network big data sharing, Digital Commun. Netw., 3, 226, 10.1016/j.dcan.2017.06.001 Wei, 2020, Intent-based networks for 6G: insights and challenges, Digital Commun. Netw., 6, 270, 10.1016/j.dcan.2020.07.001 Hamdoun, 2020, Information security through controlled quantum teleportation networks, Digital Commun. Netw., 6, 463, 10.1016/j.dcan.2020.04.009 Rauthan, 2021, Vrs-db: preserve confidentiality of users' data using encryption approach, Digital Commun. Netw., 7, 62, 10.1016/j.dcan.2019.08.001 Sha, 2020, A survey of edge computing-based designs for iot security, Digital Commun. Netw., 6, 195, 10.1016/j.dcan.2019.08.006 Chen, 2019, Embedded partitioning real-time operating system based on microkernel, 205 Yang, 2019, Real-time system modeling and verification through labeled transition system analyzer, IEEE Access, 7, 26314, 10.1109/ACCESS.2019.2899761 Nipkow, 2002