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, the success of software projects with the current technologies cannot be assured. For large complex projects, many approaches have proven inadequate to assure the correct behavior of the delivered software, despite the efforts of the (often very skilled) software engineers involved. The lack of formalization in key places makes software engineering overly sensitive to the weaknesses that are inevitable in the complex activities behind software creation. Developing large software systems is an increasingly complex task, because the systems are huge, with very complex behavior, and many algorithms employed today are “pushing the limits” of what people can comprehend. This is where formal methods have a significant opportunity.
Formal methods (FMs) 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, the maturing of formal techniques into real-life software engineering involves providing notations and tools that are readily understood and used by practitioners, and the integration of such tools with activities that are far from the unrealistic assumptions that characterized some earlier research in formal methods.
After decades of research, and despite significant advancements, formal methods are still not widely used in industrial software development. This may be due to the fact that the formal methods community has not enough focused its attention to software engineering needs, and its specific role in the software process. At the same time, from a software engineering perspective, there could be a number of fundamental principles that might help to guide the design of formal methods in order to make them more easily applicable in the development of software applications. The goal of the FormaliSE workshop series 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.