- General Chairs:
- Stefania Gnesi,
- Nico Plat,
- Program Chairs:
- Paola Spoletini,
- Patrizio Pelliccione
Welcome to FormaliSE 2018, the FME International Conference on Formal Methods in Software Engineering. FormaliSE is a yearly conference on Formal Methods in Software Engineering, and it is organized by FME (Formal Methods Europe). After 5 years as a successful satellite workshop of ICSE, this year FormaliSE is co-located with ICSE (International Conference on Software Engineering) 2018 (https://conf.researchr.org/home/icse-2018).
The software industry has a long-standing and well-earned reputation for failing to deliver on its promises and it is clear that still nowadays, even considering the current technologies, the success of software projects is often not guaranteed. Many of the approaches used for large complex problems have not been able to assure the correct behavior of the delivered software, despite the efforts of the (often very qualified and skilled) software engineers involved. This is where formal methods have a significant opportunity. In fact, formal methods are intended to provide the means for greater precision in both thinking and documenting the preliminary stage of the software creation process. When done well, this can aid all aspects of software creation: user requirement formulation, implementation, verification/testing, and the creation of documentation.
However, after decades of research, and despite significant advancement, formal methods are still not widely used in industrial software development. We believe that software engineering might help in making formal methods more easily applicable in the development of software applications, integrable into development processes, and in making more evident the return on investment (ROI) in using them. The main goal of the conference is to foster integration between the formal methods and the software engineering communities with the purpose to examine the link between the two more carefully than is currently the case.
Proceeding Downloads
Risk management for high tech systems
How do we ensure that self-driving cars, nuclear power plants and Internet-of-things devices are safe and reliable? That is the topic of risk management. Fault tree analysis is a very popular technique here, deployed by many institutions like NASA, ESA, ...
Formal verification of complex robotic systems on resource-constrained platforms
- Mohammed Foughali,
- Bernard Berthomieu,
- Silvano Dal Zilio,
- Pierre-Emmanuel Hladik,
- Félix Ingrand,
- Anthony Mallet
Software constitutes a major part of the development of robotic and autonomous systems and is critical to their successful deployment in our everyday life. Robotic software must thus run and perform as specified. Since most of these systems are used in ...
Extending specification patterns for verification of parametric traces
This article proposes a temporal and parametric specification language (PARTRAP) developed for the verification of execution traces. The language extends specification patterns with nested scopes, real-time and first-order quantification over the data ...
Runtime verification of hyperproperties for deterministic programs
In this paper, we consider the runtime verification problem of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally ...
Testing meets static and runtime verification
Test driven development (TDD) is a technique where test cases are used to guide the development of a system. This technique introduces several advantages at the time of developing a system, e.g. writing clean code, good coverage for the features of the ...
CIL to Java-bytecode translation for static analysis leveraging
A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. The overall ...
Modeling time in Java programs for automatic error detection
Modern programming languages, such as Java, represent time as integer variables, called timestamps. Timestamps allow developers to tacitly model incorrect time values resulting in a program failure because any negative value or every positive value is ...
Domain-specific design of patient classification in cancer-related cachexia research
We apply an IDE for user-level process design and composition to a real-life case study: a complex workflow from an ongoing global cancer-related cachexia research project. Originally buried in a manually operated spreadsheet, the process is now fully ...
Self-adaptive automata
Self-adaptive systems aim to efficiently respond to a wide range of changes in their operational environment by dynamically altering their behaviour. Such systems are typically comprised of a base system, implementing core functionality, and an ...
Formal verification of an autonomous wheel loader by model checking
In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks ...
Formal verification of automotive embedded software
The ever-increasing complexity of automotive embedded systems and the need for safe advanced driver assistance systems (ADAS) represent a great challenge for car manufacturers. Furthermore, we expect that in the near future, authorities require a ...
- Proceedings of the 6th Conference on Formal Methods in Software Engineering