Provably Correct Systems: Community, Connections, and Citations

  • Jonathan P. BowenEmail author
Part of the NASA Monographs in Systems and Software Engineering book series (NASA)


The original European ESPRIT ProCoS I and II projects on Provably Correct Systems took place around a quarter of a century ago. Since then, the legacy of the initiative has spawned many researchers with careers in formal methods, forming a community of researchers with a common interest in this area. This chapter uses one of the leaders on the ProCoS initiative, Ernst-Rüdiger Olderog, as an example in demonstrating connections within and around the ProCoS research community. This is formalized using the Z notation to make the description more precise, especially with respect to collaborations undertaken through coauthorship of publications and subsequent citations to this research output. Matching visualizations of the relationships are included. The social science concept of a Community of Practice (CoP) is introduced in this context. Finally, consideration of citation metrics is also included.


Citation Count Main Author Individual Publication Duration Calculus Citation Metrics 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



Jonathan Bowen is grateful for financial support from Museophile Limited. Thank you to Microsoft for the Academic Search facility, which provided the screenshots for the figures in this chapter. Many thanks to collaborators on the ProCoS projects and Working Group during the 1990s and subsequently. A special thank you to Prof. Dr Ernst-Rüdiger Olderog of Oldenburg University for the individual case study. The Z notation in this chapter has been formatted using the oz.sty Open image in new window  style and type-checked using the Open image in new window  type-checker [38]. Finally, the reviewers provided helpful comments that improved the presentation and content of the chapter.


  1. 1.
    Berners-Lee, T.: Weaving the Web: The Original Design and Ultimate Destiny of the World Wide Web. HarperCollins, New York (2000)Google Scholar
  2. 2.
    Bjørner, D., Hoare, C.A.R., Bowen, J.P., He, J., Langmaack, H., Olderog, E.R., Martin, U.H., Stavridou, V., Nielson, F., Nielson, H.R., Barringer, H., Edwards, D., Løvengreen, H.H., Ravn, A.P., Rischel, H.S.: A ProCoS project description. Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS) 39, 60–73 (1989). OctGoogle Scholar
  3. 3.
    Boca, P.P., Bowen, J.P., Siddiqi, J. (eds.): Formal Methods: State of the Art and New Directions. Springer, Heidelberg (2010)Google Scholar
  4. 4.
    Bowen, J.P. (ed.): Towards Verified Systems, Real-Time Safety Critical Systems, vol. 2. Elsevier, Amsterdam (1994)Google Scholar
  5. 5.
    Bowen, J.P.: Z: A formal specification notation. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods: An Overview Using a Case Study, chap. 1, pp. 3–19. FACIT series, Springer, Heidelberg (2001)Google Scholar
  6. 6.
    Bowen, J.P.: A relational approach to an algebraic community: From Paul Erdős to He Jifeng. In: Liu, Z., Woodcock, J.C.P., Zhu, H. (eds.) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol. 8051, pp. 54–66. Springer, Heidelberg (2013)Google Scholar
  7. 7.
    Bowen, J.P.: The Z notation: whence the cause and whither the course? In Liu, Z., Zhang, Z. (eds.) Engineering Trustworthy Software Systems: First International School, SETSS 2014, Chongqing, China, September 8–13, 2014. Lecture Notes in Computer Science, vol. 9506, pp. 104–151. Springer, Heidelberg (2016)Google Scholar
  8. 8.
    Bowen, J.P.: Alan Turing: virtuosity and visualisation. In Bowen, J.P., Diprose, G., Lambert, N. (eds.) EVA London 2016 Conference Proceedings. Electronic Workshops in Computing (eWiC), pp. 197–204. BCS (2016)Google Scholar
  9. 9.
    Bowen, J.P.: ProCoS – Provably Correct Systems. Formal Methods Wiki, Wikia. (Accessed June 2016)
  10. 10.
    Bowen, J.P., Fränzle, M., Olderog, E.R., Ravn, A.P.: Developing correct systems. In: Proceedings of the 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland. pp. 176–189. IEEE Computer Society Press, Washington (1993)Google Scholar
  11. 11.
    Bowen, J.P., Giannini, T.: Galois connections: mathematics, art, and archives. In: Ng, K., Bowen, J.P., Lambert, N. (eds.) EVA London 2015 Conference Proceedings, pp. 176–183. Electronic Workshops in Computing (eWiC), BCS (2015)Google Scholar
  12. 12.
    Bowen, J.P., Hinchey, M.G.: Formal methods. In: Gonzalez, T.F., Diaz-Herrera, J., Tucker, A.B. (eds.) Computing Handbook, vol. 1, 3rd edn., Chap. 71, pp. 1–25. CRC Press, Florida (2014)Google Scholar
  13. 13.
    Bowen, J.P., Reeves, S.: From a community of practice to a body of knowledge: a case study of the formal methods community. In: Butler, M., Schulte, W. (eds.) FM 2011: 17th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 6664, pp. 308–322. Springer, Heidelberg (2011)Google Scholar
  14. 14.
    Bowen, J.P., Wilson, R.J.: Visualising virtual communities: From Erdős to the arts. In: Dunn, S., Bowen, J.P., Ng, K. (eds.) EVA London 2012 Conference Proceedings. pp. 238–244. Electronic Workshops in Computing (eWiC), BCS (2012). arXiv:1207.3420v1
  15. 15.
    Bowen, J.P., et al.: A ProCoS II project description: ESPRIT Basic Research project 7071. Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS) 50, 128–137 (1993)Google Scholar
  16. 16.
    Bowen, J.P., et al.: A ProCoS-WG Working Group description: ESPRIT Basic Research 8694. Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS) 53, 136–145 (1994). JunGoogle Scholar
  17. 17.
    Breuer, P.T., Bowen, J.P.: Empirical patterns in Google Scholar citation counts. In: Proceedings of the IEEE 8th International Symposium on Service Oriented System Engineering (SOSE), Cyberpatterns 2014: Third International Workshop on Cyberpatterns. pp. 398–403. IEEE Computer Society Press, Washington (2014). arXiv:1401.1861 [cs.DL]
  18. 18.
    Brezina, V.: Use of Google Scholar in corpus-driven EAP research. J. Engl. Acad. Purp. 11(4), 319–331 (2012). DecGoogle Scholar
  19. 19.
    Egghe, L.: Theory and practise of the g-index. Scientometrics 69(1), 131–152 (2006)CrossRefGoogle Scholar
  20. 20.
    Harré, R.: The Philosophies of Science: An Introductory Survey. Oxford University Press, Oxford (1972)Google Scholar
  21. 21.
    He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. International Series in Software Engineering. McGraw-Hill, New York (1995)Google Scholar
  22. 22.
    He, J., Bowen, J.P.: Specification, verification and prototyping of an optimized compiler. Form. Asp. Comput. 6(6), 643–658 (1994)CrossRefzbMATHGoogle Scholar
  23. 23.
    He, J., Hoare, C.A.R., Fränzle, M., Müller-Olm, M., Olderog, E.R., Schenke, M., Hansen, M.R., Ravn, A.P., Rischel, H.: Provably correct systems. In: Langmaack, H., de Roever, W.P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 863, pp. 288–335. Springer, Heidelberg (1994)Google Scholar
  24. 24.
    Henson, M.C., Reeves, S., Bowen, J.P.: Z logic and its consequences. CAI Comput. Inf. 22(4), 381–415 (2003)Google Scholar
  25. 25.
    Hirsch, J.E.: An index to quantify an individual’s scientific research output. In: Proceedings of the National Academy of Sciences 102(46), 16569–16572 (2005). arXiv:physics/0508025
  26. 26.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. International Series in Computer Science. Prentice Hall, New Jersey (1998)Google Scholar
  27. 27.
    Hoare, C.A.R., He, J., Bowen, J.P., Pandya, P.K.: An algebraic approach to verifiable compiling specification and prototyping of the ProCoS level 0 programming language. In: ESPRIT’90 Conference Proceedings, Brussels. pp. 804–818. CEC DG XIII (1990)Google Scholar
  28. 28.
    Katsaros, D., Akritidis, L., Bozanis, P.: The f index: quantifying the impact of coterminal citations on scientists’ ranking. J. Assoc. Inf. Sci. Technol. 60(5), 1051–1056 (2009). MayCrossRefGoogle Scholar
  29. 29.
    Langmaack, H., Ravn, A.P.: The ProCoS project: provably correct systems. In: Bowen [4], pp. 249–265, appendix BGoogle Scholar
  30. 30.
    Lanville, A.N., Meyer, C.D.: Google’s PageRank and Beyond: The Science of Search Engine Rankings. Princeton University Press, PrincetonGoogle Scholar
  31. 31.
    Moore, J.S., et al.: Special issue on system verification. J. Autom. Reas. 5(4), 409–530 (1989). DecGoogle Scholar
  32. 32.
    Olderog, E.R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press, Cambridge (1991)Google Scholar
  33. 33.
    Olderog, E.R.: Interfaces between languages for communicating systems. In: Kuich, W. (ed.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623, pp. 641–655. Springer, Heidelberg (1992). (invited paper)Google Scholar
  34. 34.
    Olderog, E.R. (ed.): Programming Concepts, Methods and Calculi, IFIP Transactions, vol. A-56. North-Holland (1994)Google Scholar
  35. 35.
    Parnas, D.L.: Stop the numbers game. Commun. ACM 50(11), 19–21 (2007). NovCrossRefGoogle Scholar
  36. 36.
    Sanitt, N.: Graph theory. In: Science as a Questioning Process, Chap. 3, pp. 31–49. Institute of Physics Publishing (1996)Google Scholar
  37. 37.
    Spivey, J.M.: The Z Notation: A reference manual. Prentice Hall (1989/1992/2001).
  38. 38.
    Spivey, J.M.: The f uzz type-checker for Z. Technical report, University of Oxford, UK (2008).
  39. 39.
    Van Doren, C.: A History of Knowledge: Past, Present, and Future. Ballantine Books (1991)Google Scholar
  40. 40.
    Wenger, E.: Communities of Practice: Learning, Meaning, and Identity. Cambridge University Press, Cambridge (1998)Google Scholar
  41. 41.
    Wenger, E., McDermott, R.A., Snyder, W.: Cultivating Communities of Practice: A guide to managing knowledge. Harvard Business School Press, Massachusetts (2002)Google Scholar
  42. 42.
    Young, W.D.: System verification and the CLI stack. In: Bowen [4], pp. 225–248, appendix AGoogle Scholar
  43. 43.
    Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991). DecMathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.School of EngineeringLondon South Bank UniversityLondonUK

Personalised recommendations