Formal Methods play a major role in computer engineering and in the broader context of software and systems engineering, where also the interaction of machines with humans is taken into consideration. In fact:
All engineering disciplines make progress by employing mathematically based notations and methods. Research on formal methods follows this model and attempts to identify and develop mathematical approaches that can contribute to the task of creating computer systems (both their hardware and software components). Cliff Jones, Thinking Tools for the Future of Computing Science 1)
The very origins of FM go back to Mathematical Logic, or, more precisely, to that branch of Mathematical Logic which gave rise to Logics in Computer Science (LICS) and Theoretical Computer Science (TCS). Several fields of LICS and TCS have contributed to the development of the foundations of FM, like language and automata theory, Petri nets, programming/specification language syntax and semantics, and program verification.
More recently, solid contributions to the specification and analysis of systems, in particular concurrent/distributed systems have been provided. Among them we recall process algebras, temporal logics, and model checking.
It occurred to me that often complex communication and synchronization protocols were specified by state machines and that an efficient algorithm for checking formulas on models could be used to see if the state machines satisfied their specifications. This was my “Eureka moment”! I realized that the important problem for verification was not the synthesis problem but the problem of checking formulas on finite models. I began to work on a depth-first search algorithm for the Model Checking problem.
Edmund M. Clarke (1945-2020), The Birth of Model Checking 2)
The Formal Methods and Tools (FMT) lab has longstanding experience in the development and application of formal notations, methods and software support tools for the specification, design and verification of complex systems. These efforts are typically based on the foundational concepts and techniques of process algebras, temporal logics, spatial logics, and model checking. FMT is also active in requirements engineering and various branches of software engineering, and in the areas of computer ethics and information technology and society. Important application fields concern the railway domain and, recently, medical image analysis.
The FMT Lab is part of the Institute of Information Science and Technologies (ISTI), one of the institutes of the Italian National Research Council (CNR).
1)
Cliff Jones, Thinking Tools for the Future of Computing Science. In R. Wilhelm, editor, Informatics 10 Years Back 10 Years Ahead, Lecture Notes in Computer Science, volume 2000. Springer, 2000.
2)
Edmund M. Clarke, The Birth of Model Checking. In O. Grumberg and H. Veith, editors, 25 Years of Model Checking: History, Achievements, Perspectives, Lecture Notes in Computer Science, volume 5000. Springer, 2008.
Obituary Edmund M. Clarke