Abstract
This contribution reports of work done after the official end of the ProCoS project in 1995. Most of this work was done while the author was affiliated with Bremen University. The aim of this contribution is to show the effect of ProCoS on these projects, which comprises analysis of systems from two different application domains: space and aerospace. In both examples, the basic approach involves abstraction to CSP specifications and model-checking using FDR. Another common factor is the use of other techniques in combination with model-checking.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Buth, B.: Formal and Semi-Formal Methods for the Analysis of Industrial Control Systems. Bremen University (2002)
Buth, B.: Analysing mode confusion: an approach using FDR2. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, vol. 3219, pp. 101–114. Springer, Heidelberg (2004)
Buth, B., Peleska, J.: Formal methods for large-scale industrial applications – deadlock and livelock analysis for the international space station. In: Tutorial Material for the Advanced Summer School in Formal Methods and Applications, Beijing, China, October 1999
Buth, B., Cardell-Oliver, R., Peleska, J.: Combining tools for the verification of fault-tolerant systems. In: Berghammer, R., Buth, B., Peleska, J. (eds.) Tools for Software Development and Verification. BISS Monographs, vol. 1. Shaker-Verlag (1996) (in print)
Buth, B., Kouvaras, M., Peleska, J., Shi, H.: Deadlock analysis for a fault-tolerant system. In: Johnson, M. (ed.) Algebraic Methodology and Software Technology. Proceedings of AMAST’97. LNCS, vol. 1349 , pp. 60–75. Springer, December 1997
Buth, B., Peleska, J., Shi, H.: Combining methods for the analysis of a fault-tolerant system. In: Haeberer, A.M. (ed.) Algebraic Methodology and Software Technology, Proceedings of AMAST’98. LNCS, vol. 1548, pp. 124–139. Springer, January 1999
Buth, B., Peleska, J., Shi, H.: Combining methods for the analysis of a fault-tolerant system. In: Proceedings of Quality Week ’99, May 1999. (CDrom)
Davies, J.: Specification and Proof in Real-Time CSP. Cambridge University Press, New York (1993)
Dill, D.: The mur\(\phi \) verification system. In: Alur, R., Henzinger, T. (eds.) Computer Aided Verification, CAV’96. LNCS, vol. 1102. Springer, Heidelberg (1996)
Formal Systems (Europe) Lts. FDR2 User Manual, FDR 2.97 edition. http://www.fsel.com/documentation/fdr2/html/fdr2manual.html
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 8413, pp. 187–201. Springer, Heidelberg (2014)
Hoare, C.A.R.: Communicating Sequential Processes. Red Series. Prentice-Hall International, Englewood Cliffs (1985)
inmos ltd. occam 2 Reference Manual. Series in Computer Science. Prentice Hall International (1988)
Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982)
Leveson, N.G., Palmer, E.: Designing automation to reduce operator errors. In: Proceedings of the IEEE Systems, Man, and Cybernetics Conference (1997)
Levevson, N.G., Pinnel, L.D., Sandys, S.D., Koga, S., Rees, J.D.: Analyzing software specifications for mode confusion potential. In: Johnson, C.W. (ed.) Proceedings of a Workshop on Human Error and System Development, Glasgow, Scotland, Glasgow Accident Analysis Group, Technical Report GAAG-TR-97-2, pp. 132–146, March 1997
Lüttgen, G., Carreño, V.: Analyzing mode confusion via model checking. Technical Report NASA/CR-1999-209332, ICASE Report No. 99-18, ICASE - NASA Langley Research Center, May 1999. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.95.5171&rep=rep1&type=pdf
Miller, S.P., Potts, J.N.: Detecting mode confusion through formal modeling and analysis. Technical Report NASA/CR-1999-208971, NASA Langley Research Center, January 1999. https://shemesh.larc.nasa.gov/fm/papers/Miller-99-cr208971-Mode-Confusion.pdf
Palmer, E.: Oops, it didn’t arm. A case study of two automation surprises. In: Jensen, R.S., Rakovan, L.A. (eds.) Proceedings of the 8th International Symposium on Aviation Psychology, Columbus, OH, The Aviation Psychology Department of Aerospace Engineering, Ohio State University, pp. 227–232, April 1995.
Peleska, J., Buth, B.: Formal methods for the international space station iss. In: Olderog, E.R., Steffen, B. (eds.) Correct System Design - Recent Insights and Advances. Lecture Notes in Computer Science, vol. 1710, pp. 363–389. Springer, Heidelberg (1999)
Peleska, J., Shi, H., Kouvaras, M.: Combining methods for the analysis of a fault-tolerant system. In: Proceedings of the 1999 Pacific Rim International Symposium on Dependable Computing (PRDC 1999) (1999) (Submitted)
Rushby, J., Crow, J., Palmer, E.: An automated method to detect potential mode confusions. In: 18th AIAA/IEEE Digital Avionics Systems Conference, St. Louis (MO) (1999)
Roscoe, A.W.: Model-checking CSP. In: A Classical Mind, Eassys in Honour of C.A.R. Hoare. Prentice-Hall International (1997)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Upper Saddle River (1997)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Upper Saddle River (1998)
Roscoe, A.W.: Understanding Concurrent Systems, 1st edn. Springer, New York (2010)
Rushby, J.: Using model checking to help discover mode confusion and other automation surprises. In: Proceedings of the 3rd Workshop on Human Error, Safety, and System Development (HESSD’99), Liege, Belgium (1999)
Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. In: Reliability Engineering and System Safety (2002)
Sarter, N.B., Woods, D.D., Billings, C.E.: Automation surprises. In: Salvendy, G. (ed.) Handbook of Human Factors and Ergonomics. Wiley, New York (1997)
Schrönen, M.: Methodology for the Development of Microprocessor-Based Safety-Critical Systems. Monographs of the Bremen Institute of Safet Systems 8, Bremen University (1998). Shaker Verlag, Aachen
Schneider, S.: Concurrent and Real-Time Systems: The CSP Approach. Wiley, New York (1999)
Twele, L., Schlingloff, H., Szczerbicka, H.: Performability analysis of an avionics-interface. In: Proceedings of IEEE Conference on Systems, Man and Cybernetics, San Diego, N.J., pp. 499–504 (1998)
University of Oxford. FDR3 User Manual, FDR 3.4 edition. https://www.cs.ox.ac.uk/projects/fdr/manual/index.html
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Buth, B. (2017). From ProCoS to Space and Mental Models–A Survey of Combining Formal and Semi-formal Methods. In: Hinchey, M., Bowen, J., Olderog, ER. (eds) Provably Correct Systems. NASA Monographs in Systems and Software Engineering. Springer, Cham. https://doi.org/10.1007/978-3-319-48628-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-48628-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48627-7
Online ISBN: 978-3-319-48628-4
eBook Packages: Computer ScienceComputer Science (R0)