Related Research Articles
The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go, Crystal, and Clojure's core.async.
Mondex was a smart card electronic cash system, implemented as a stored-value card and owned by Mastercard.
Jonathan P. Bowen FBCS FRSA is a British computer scientist and an Emeritus Professor at London South Bank University, where he headed the Centre for Applied Formal Methods. Prof. Bowen is also the Chairman of Museophile Limited and has been a Professor of Computer Science at Birmingham City University, Visiting Professor at the Pratt Institute, University of Westminster and King's College London, and a visiting academic at University College London.
The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
Jean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.
Clifford "Cliff" B. Jones is a British computer scientist, specializing in research into formal methods. He undertook a late DPhil at the Oxford University Computing Laboratory under Tony Hoare, awarded in 1981. Jones' thesis proposed an extension to Hoare logic for handling concurrent programs, rely/guarantee.
Unifying Theories of Programming (UTP) in computer science deals with program semantics. It shows how denotational semantics, operational semantics and algebraic semantics can be combined in a unified framework for the formal specification, design and implementation of programs and computer systems.
He Jifeng is a Chinese computer scientist.
The Information Technology Security Evaluation Criteria (ITSEC) is a structured set of criteria for evaluating computer security within products and systems. The ITSEC was first published in May 1990 in France, Germany, the Netherlands, and the United Kingdom based on existing work in their respective countries. Following extensive international review, Version 1.2 was subsequently published in June 1991 by the Commission of the European Communities for operational use within evaluation and certification schemes.
Kevin C. Lano is a British computer scientist.
Prentice Hall International Series in Computer Science was a series of books on computer science published by Prentice Hall.
Michael Spivey is a British computer scientist at the University of Oxford.
Jeannette Marie Wing is Avanessians Director of the Data Science Institute at Columbia University, where she is also a professor of computer science. Until June 30, 2017, she was Corporate Vice President of Microsoft Research with oversight of its core research laboratories around the world and Microsoft Research Connections. Prior to 2013, she was the President's Professor of Computer Science at Carnegie Mellon University, Pittsburgh, Pennsylvania, United States. She also served as assistant director for Computer and Information Science and Engineering at the NSF from 2007 to 2010. She was appointed the Columbia University executive vice president for research in 2021.
Jim Davies is Professor of Software Engineering and current Director of the Software Engineering Programme at the University of Oxford, England.
Professor Martin C. Henson FBCS FRSA is an English computer scientist based at the University of Essex. He is dean for international affairs and is affiliated to the School of Computer Science & Electronic Engineering. Henson was head of the department of computer science from 2000 to 2006.
Steve Reeves is a computer scientist based at the University of Waikato in New Zealand. He has been in the various roles of Associate Dean, Programme Co-ordinator and Head of Department of Software Engineering. He has undertaken research work on the Z notation, formal methods for GUI design, a general theory of refinement and logic for veracity.
Charles Carroll Morgan is an American computer scientist who moved to Australia in his early teens. He completed his education there, including a Doctor of Philosophy (Ph.D.) degree from the University of Sydney, and then moved to the United Kingdom in the early 1980s. In 2000, he returned to Australia.
Kenneth ("Ken") Arthur Robinson was an Australian computer scientist. He has been called "The Father of Formal Methods in Australia".
References
- ↑ Jim Woodcock homepage, Oxford University Computing Laboratory.
- ↑ Official homepage, University of York, UK.
- ↑ Jim Woodcock and Jim Davies, Using Z: Specification, Refinement, and Proof. Prentice-Hall International Series in Computer Science, 1996. ISBN 978-0-13-948472-8
- ↑ The Queen's Award for Technological Achievement 1992 Archived 2 December 2008 at the Wayback Machine , Oxford University Computing Laboratory, UK.
- ↑ Jim Woodcock, Susan Stepney, David Cooper, John Clark, and Jeremy Jacob, The certification of the Mondex electronic purse to ITSEC Level E6, Formal Aspects of Computing , Volume 20, Number 1, pages 5–19, January 2008.
- ↑ "Editors". Formal Aspects of Computing . Springer . Retrieved 23 February 2019.
