Formal methods have been applied more and more in industrial circles. They use mathematical logic and rigorous models for analysis and verification, can be used at all the system life cycles, and provide verified software without bugs with respect to certain properties. The increasing industrial applications show that formal methods not only are theoretical research anymore, but also can be deployed in many concrete industrial applications. This paper surveys the important formal specification and verification of system-Level achievements in industrial circles.

Feng Zhang, Wensheng Niu, A Survey on Formal Specification and Verification of System-Level Achievements in Industrial Circles. Academic Journal of Computing & Information Science (2019) Vol. 2: 22-34. https://doi.org/10.25236/AJCIS.010015.

[1] Formal Methods Europe. Formal methods. http://www. fmeurope.org/ formalmethods.
[2] Jean-Raymond Abrial. Formal methods: Theory becoming practice. Journal of Universal Computer Science, 2007, 13 (5): 619-628.
[3] Woodcock J., Larsen P. G., Bicarregui J., et al. Formal methods: Practice and experience. ACM computing surveys (CSUR), 2009, 41 (4): 19: 1-19: 36.
[4] Zhao Yongwang, Ma Dianfu, and Yang Zhibin. 2014 A survey on formal specification and verification of separation kernels. Technical report, Tech. rep., National Key Laboratory of Software Development Environment (NLSDE). Beihang Univerisity.
[5] Zhao Yongwang., Sanán David, Zhang Fuyuan, et al. High-assurance separation kernels: a survey on formal methods. arXiv preprint arXiv:1701.01535, 2017.
[6] Berry, G. 2008. Synchronous design and verification of critical embedded systems using SCADE and Esterel. Lecture Notes in Computer Science, In Formal Methods for Industrial Critical Systems. Heidelberg: Springer, 2008, 4916: 2-2.
[7] Souyris, J. , Wiels, V. , Delmas, D., et al. Formal Verification of Avionics Software Products. Proceedings of The International symposium on formal methods. Berlin: Springer, 2009: 532-54.
[8] Guiho G. and Hennebert C.. SACEM software validation. Proceedings of the 12th International Conference on Software Engineering. Nice: IEEE Computer Society Press, 1990: 186-191.
[9] Hennebert C. and Guiho G.. SACEM: A fault tolerant system for train speed control. Proceedings of the 23th International Symposium on Fault-Tolerant Computing. Toulouse, France: IEEE Computer Society Press, 1993: 624-628.
[10] Jonathan Bowen and Victoria Stavridou. Safety-Critical Systems, Formal Methods and Standards. Software Engineering Journal, 1993, 8 (4): 189-209.
[11] Jean-Raymond Abrial. The B-book: Assigning Programs to Meanings. Cambridge: Cambridge University Press, 1996.
[12] Behm P., Benoit P., Faivre A, et al. M\eteor: A successful application of B in a large project. International Symposium on Formal Methods. Berlin, Heidelberg: Springer, 1999: 369-387.
[13] Badeau F. and Amelot A. Using B as a high level programming language in an industrial project: Roissy VAL. International Conference of B and Z Users. Berlin, Heidelberg: Springer, 2005: 334-354.
[14] Klein G., Elphinstone K., Heiser G., et al. seL4: Formal verification of an OS kernel. Proceedings of the 22nd ACM Symposium on Operating Systems Principles. ACM, 2009: 207-220.
[15] Murray T., Matichuk D., Brassil M., et al. seL4: From General Purpose to a Proof of Information Flow Enforcement. Proceedings of The IEEE Symposium on Security and Privacy. IEEE Press, 2013: 415-429.
[16] GreenHills. INTEGRITY-178B RTOS. http://www.ghs.com/products/safety critical/integrity-do-178b.html. (2015). Accessed: 2015-07.
[17] Common Criteria. Common criteria for information technology security evaluation (3.1 r4 ed.). National Security Agency, 2012.
[18] National Information Assurance Partnership (NIAP). Separation Kernels on Commodity Workstations. http://www.niap-ccevs.org/ announcements/ Separation\%20Kernels\%20on\%20Commodity\%20Workstations.pdf. 2010.
[19] Greve, David, Matthew Wilding, and W. Mark Vanfleet. A Separation Kernel Formal Security Policy. Proceedings of The Fourth International Workshop on the ACL2 Theorem Prover and Its Applications. 2003.
[20] Liang Gu, Alexander Vaynberg, Bryan Ford, et al. CertiKOS: a certified kernel for secure cloud computing. Proceedings of the Second Asia-Pacific Workshop on Systems. ACM, 2011: 3.
[21] Gu R., Koenig J., Ramananandro T., et al. Deep specifications and certified abstraction layers. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - (POPL). 2015: 595-608.
[22] Appel A. W., Beringer L., Chlipala A., et al. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 2017, 375 (2104): 20160331.
[23] Xavier Leroy. The CompCert C verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt, March 2012. http://compcert. inria.fr/man/ manual.pdf.
[24] David Costanzo, Zhong Shao, and Ronghui Gu. End-to-end Verification of Information-flow Security for C and Assembly Programs. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). In Proc. of PLDI’16. ACM Press, 2016: 648-664.
[25] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52 (7): 107–115.
[26] John McCarthy and James Painter. Correctness of a compiler for arithmetical expressions. Proceedings of the Symposia in Applied Mathematics. American Mathematical Society, 1967: 33–41
[27] Robin Milner and Richard Weyrauch. Proving compiler correctness in a mechanized logic. Proceedings of the 7th Annual Machine Intelligence Workshop. Edinburgh University Press, 1972: 51–72.
[28] CompCert. See http://compcert.inria.fr.
[29] Franca RB, Favre-Felix D, Leroy X, Pantel M, Souyris J. Towards formally verified optimizing compilation in flight control software [A]. Proceedings of The Predictability and Performance in Embedded Systems (PPES), 2011, 18: 59-68.
[30] Owre, S., Rushby, J. M., and Shankar, N.. PVS: A prototype verification system. Proceedings of 11th International Conference on Automated Deduction. Berlin: Springer, 1992: 748-752.
[31] Miller S.P. and Srivas M.. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods.Proceedings of 1995 IEEE Workshop on Industrial-Strength Formal Specification Techniques. Boca Raton: IEEE, 1995: 2-16.
[32] Srivas, M. and Miller, S.. Applying formal verification to a commercial microprocessor. In IFIP Conference on Hardware Description Languages and their Applications (CHDL). Makuhari, Chiba, Japan: IEEE, 1995.
[33] Miller, S. P., Greve, D. A., and Srivas, M. K.. Formal verification of the AAMP5 and AAMP-FV microcode. Proceedings of the Third AMAST Workshop on Real-Time Systems. Salt Lake City, Utah. 1996.
[34] Greve D. and Wilding M.. Evaluatable, high-assurance microprocessor. Proceedings of the Second Annual HighConfidence Systems and Software Conference (HCSS). National Security Agency, Linthicum, 2002.
[35] Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: ACL2 Case Studies. Springer Science \& Business Media, Vol. 4.
[36] Barrett G. occam 3 reference manual. Inmos Limited, March 1992. Available at: http://wotug. ukc. ac. uk/parallel/occam/documentation, 1992.
[37] Wexler J. Concurrent programming in OCCAM 2. New York: Ellis Horwood, 1989.
[38] May David, and Roger Shepherd. The transputer. Neural Computers. Springer, 1989. 477-48.
[39] Spivey J. M. and Abrial J.-R.. The Z Notation, second edition. Prentice Hall International, Hemel Hempstead (U.K.), 1992.
[40] Woodcock, J. and Davies, J.. Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall, 1996.
[41] Geoff Barrett. Formal methods applied to a floating-point number system. IEEE transactions on software engineering, 1989, 15 (5): 611-621.
[42] Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12 (10): 576-580.
[43] Barrett, G.. 1990. Verifying the Transputer. Proceedings of the first conference of the North American Transputer Users Group on Transputer research and applications.  IOS Press, 1990.
[44] Jeremy Gibbons. Formal methods: Why should I care? The development of the T800 Transputer floating-point unit. Proceedings of the 13th New Zealand Computer Society Conference. Auckland: New Zealand Computer Society, 1993: 207-217.
[45] Kathleen Fisher. HACMS: High assurance cyber military systems. Proceedings of the 2012 ACM Conference on High Integrity Language Technology. Boston, USA, 51–52.
[46] Fisher K., Launchbury J., Richards R.. The HACMS program: using formal methods to eliminate exploitable bugs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences,  2017: 375 (2104), 20150401.