Behavioral specification theories are specification formalisms in which specifications have an operational interpretation and models are verified by comparing their operational behavior against the specification’s behavior. They come equipped with logical and structural operations which permit compositional and incremental design.
I will give a high-level introduction to behavioral specification theories, followed by specific incarnations and an overview of the state of the art, including the relation between specification theories and contracts. I will finish by an outlook onto how I believe behavioral specification theories can be useful in the rigorous design of cyber-physical systems.
This talk is based on joint work with Nikola Beneš, Benoît Delahaye, Jan Křetínský, Axel Legay, and Louis-Marie Traonouez.
Ulrich Fahrenberg has started his career in computer science as an assistant professor at Aalborg University. Afterwards he has worked as a postdoc at Inria Rennes, France, and since 2016 he is a researcher at the computer science lab at École polytechnique in Palaiseau, France. He works in algebraic topology, concurrency theory, real-time verification, and general quantitative verification. He has published more than 60 papers in computer science and mathematics. He is a reviewer for AMS Mathematical Reviews.