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 engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, and most commonly, digital logic circuits.
A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically rigorous techniques for the specification, development 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, Go, Crystal, and Clojure's core.async.
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
A modeling language is any artificial language that can be used to express information or knowledge or systems in a structure that is defined by a consistent set of rules. The rules are used for interpretation of the meaning of components in the structure.
In computer science, graph transformation, or graph rewriting, concerns the technique of creating a new graph out of an original graph algorithmically. It has numerous applications, ranging from software engineering to layout algorithms and picture generation.
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. It was originally developed in the 1980s by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe. It has robust, commercially available tool support for specification, design, proof and code generation.
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.
In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures.
James Jay Horning was an American computer scientist and ACM Fellow.
Algebraic specification is a software engineering technique for formally specifying system behavior. It was a very active subject of CS research around 1980.
Johannes Aldert "Jan" Bergstra is a Dutch computer scientist. His work has focussed on logic and the theoretical foundations of software engineering, especially on formal methods for system design. He is best known as an expert on algebraic methods for the specification of data and computational processes in general.
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.
CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
SIGNAL is a programming language based on synchronized data-flow : a process is a set of equations on elementary flows describing both data and control.
Marie-Claude Gaudel is a French computer scientist. She is a professor emerita at the University of Paris-Sud. She helped develop PLUSS language for software specifications and was involved in both theoretical and applied computer science. Gaudel is still active in professional societies.
References
- ↑ Guttag, John V.; Horning, James J. (1993). Larch: Languages and Tools for Formal Specification (PDF). Springer-Verlag. ISBN 978-1-4612-2704-5.
