While the importance of requirements formalization has often been highlighted, the way to support this activity in industrial context has not been sufficiently addressed in current research. Since a major determinant of the quality of software systems is the quality of their requirements, these must be both understandable and precise. Natural language, the most commonly used for writing requirements, helps understandability, but lacks precision. To achieve precision, researchers have for many years advocated the use of formal approaches to writing requirements. Many requirements methods and notations are available as a result of these efforts and they vary considerably in their style, scope and applicability. Despite of this, industrial application is still limited. This workshop aims at raising fundamental questions, including how remote the current state of the technology is from potential widespread industrial usage of formal methods. The objective is also to focus on existing methods that do have industrial application and identify the reason of their success.
FormReq will bring together industrial practitioners as well as researchers to discuss the good practices, the remaining challenges, of using formal approaches to express and manage requirements.
The two keynotes will illustrate two of these challenges. The first one, presented by Xiaohong Chen from the East China Normal University, tackles the problem of verifying safety requirements for railways systems. The second one, presented by Antonio Bucchiarone from the Fondazione Bruno Kessler- IRST in Italia, deals with the definition of gamification requirements.
The five selected papers present new developments on two traditional, but always pending, challenges, namely to develop relevant verification tools for requirements specification and to bridge the gap between customer requirements and formal analysis.
10:30-12h00 session 1: Keynote
Xiaohong Chen
“Automatically Detecting Inconsistencies in Safety Requirements for Railway Systems”
13h – 14:30 session 2: formal methods use
“SpecEdit: Projectional Editing for TLA+ Specifications”, Riwan Cuinat et al., ENSTA, France
“Formalizing Security and Safety Requirements by Mapping Attack-Fault Trees on Obstacle Models with Constraint Programming Semantics”, Christophe Ponsard et al., CETIC, Respect-IT, Belgium
15:00 – 16:30 session 3: Keynote
Antonio Bucchiarone
“Requirements@Runtime: The Case of Gameful Systems”
17:00-18:30 session 4: Bridging the gap between customer requirements and formal analysis
“Formal Requirements in an Informal World”, Daniel Dietsch et al. , University of Freiburg, Germany
“Requirements-based Code Model Checking”, Ulrich Schöpp et al., fortiss GmbH and Airbus Defence and Space GmbH, Germany
“Formalization of Requirements for Correct Systems”, Jeanine Souquieres et al., LORIA, University of Luxembourg, France, Luxembourg