Programa Dia 12 - Sexta-Feira

A number of industrial projects where the presenter has been using VDM will be presented. This will be put in context of a new general survey of the state of the art in the industrial application of formal methods. We have gathered information about as many industrial formal methods applications as possible with the assistance of many different stakeholders. This presentation will be the first reporting on the different trends that have come out of this survey. Finally this presentation will look into future expected industrial trends in relation to the presenter's academic research.

Bio:  Peter Gorm Larsen studied computer science at the Technical University of Denmark (MSc 1988, PhD 1995) with focus on semantics, computer languages and tool support. He has worked in industry for most of his career. For 13 years he worked with IFAD and was the main architect of VDMTools and he was responsible for support of VDMTools world-wide. For 3,5 years he worked for Systematic Software Engineering mainly doing business development for large defense projects. He is now a full professor at the Engineering College of Aarhus and in addition has his own one-man consultancy company PGL Consult.

This talk revisits the experiences with the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable barrier which has to protect Rotterdam from floodings while, at almost the same time, not restricting  shipping traffic to the port of Rotterdam. The control system, called BOS, completely autonomously decides about closing and opening of the barrier and, when necessary, also performs these tasks without human intervention. BOS is a safety-critical software system of the highest Safety Integrity Level according to the IEC 61508 standard. One of the reliability increasing techniques used during its development is formal methods. This talk revisits the earlier published experiences with the project after the system is now in operation for ten years and has performed its first barrier operation because of a storm on November 11th, 2007.

Bio: Klaas Wijbrans studied electrical engineering at the University of Twente (Msc 1988, PhD 1993) with focus on software engineering methods for control systems.He has worked for industry in the area of high availability systems for most of his career in various positions. He was the main architect for the Storm Surge barrier near Rotterdam. For 7 years he worked with Imtech on electronic road pricing systems and license plate recognition systems. After that, he worked for 13 years with CMG/LogicaCMG/Acision, starting with the storm surge barrier, on X-ray systems and for the past 7 years on high availability telecom systems such as SMS, Multimedia Messaging and voice mail. He is now director of product management at Acision, the former telecommunications equipment division of LogicaCMG.

 

To ensure that software is right and is the right software (S), that is, that it is correct with respect to written requirements (R) and that it meets customer expectations we introduce the notion of domain descriptions (D). That is, before software can be designed (S) we must make sure we understand the requirements (R), and before we can express the  requirements we must make sure that we understand the application domain (D): the area of activity of the users of the required software, before and after installment of such software. We shall outline what we mean by informal, narrative and formal domain description, and how one can systematically, albeit not (in fact: never) automatically go from domain descriptions to requirements prescriptions. As it seems that domain engineering is a relatively new discipline within software engineering we shall mostly focus on domain engineering and discuss its necessity. he talk will show some formulas but they are really not meant to be read by the speaker, let alone understood, during the talk, by the listeners. They are merely there to bring home the point: Professional software engineering, like other professional engineering branches rely on and use mathematics. And it is all very simple to learn and practive anyway

Bio: Dines Bjørner (born October 4, 1937 in Odense) is a Danish computer scientist. He specializes in research into formal methods. He worked with Cliff Jones and others on the Vienna Development Method (VDM) at IBM inVienna (and elsewhere). Later he was involved with producing the RAISE (Rigorous Approach to Industrial Software Engineering) formal method with tool support. Bjørner has been a professor at the Technical University of Denmark (DTU) in Lyngby, close to Copenhagen, Denmark from 1965-1969 and 1976-2007, before he retired in March 2007. Inter alia, he was responsible for establishing the United Nations University International Institute for Software Technology (UNU-IIST) in Macau during the 1990s. His magnum opus on software engineering (three volumes) appears in 2005/6. To support VDM, Bjørner co-founded VDM-Europe, which subsequently became Formal Methods Europe, an organization that supports conferences and related activities. In 2003, he instigated the associated ForTIA Formal Techniques Industry Association. Dines Bjørner is a knight of the Order of the Dannebrog and won the John von Neumann Medal in Budapest, Hungary in 1994. He received a Dr.h.c. from the Masaryk University, Brno, Czech Republic in 2004. He is a Fellow of the IEEE (2004) and ACM (2005).

"Formal Methods in Industry: The World and Critical Software", José Miguel Faria  

Formal methods (FMs) can be notably valuable helping to produce complex systems that are free of design errors. Furthermore, at the highest safety-critical certification levels, their application is either highly recommended or mandatory. The presentation is intended to illustrate students the importance and industrial applicability of formal methods related technologies, motivating them to embrace such a field. The presentation shall have a broad scope, covering the following topics: description of the speaker’s personal experience and motivation, overview of existing formal languages and tools, examples of applications in large industrial projects, overview of the main markets and projects where Critical Software is (has been) involved, the role of formal methods in safety-critical certification standards,
and application of formal methods at Critical Software.

Bio: José Miguel Faria, MSc, is project engineer at Critical Software S.A. (CSW) where he is responsible for the development and applications of competences on formal methods. Mr. Faria first completed studies (5 years degree) on Mechanical Engineering, at Faculdade de Engenharia da Universidade do Porto (FEUP), Portugal. He has served as engineer at European Synchrotron Radiation Facility, France, where he leaded the construction of a series of robotic devices. During this time, he gradually developed interest on dependable systems, which led him to join the Formal Methods Group of the University of Ghent, Belgium.
There, he worked on the formal specification and validation of a new real-time operating system for embedded distributed applications (developed in cooperation with an external company, Open License Society). Back to Portugal, Mr. Faria integrated the Industrial Robotics Laboratory of the University of Coimbra and completed MSc studies in Electrical and Computers Engineering with a thesis on the application of formal methods for the development of software systems. Mr. Faria serves at CSW since August 2007.