#Suitability of procedural programs software#
After all, using formal methods requires skills that most software developers do not have, including familiarity with complex mathematical and logical structures. It also makes a difference whether engineers involved in the project are trained for a particular method and domain or whether their experiences are available for maintenance later on.
#Suitability of procedural programs verification#
For instance, the development of safety-critical systems needs elaborate evidence for compliance with safety requirements and standards, whereas other projects have budget and time restrictions that do not allow for expensive verification efforts. For example, Amazon initially applied Alloy 3 to the problem, a method that was not particularity designed for this task.ĭifferent formal methods are generally suitable for different kinds of software projects, domains, and social and economic settings. Choosing an inappropriate method for a task leads to undesired results and misconceptions about the method. Today, no help is available that navigates practitioners through the intricate process of choosing a formal method suitable for their problem domain. Such experimentations are indeed a nuisance for new adopters of formal methods (and, at times, also for previous adopters). 2 However, choosing TLA+ was not a straightforward decision for Amazon, and they experimented with other methods before finally selecting one that satisfied their needs. One such example is the use of the formal method TLA+ 1 at Amazon for specifying and model checking their web services. However, we can generate several pointers, which make this selection process a lot less cumbersome.Īfter years of advocacy, numerous success stories in the safety-critical systems domain, and the availability of various “easy to use” methods and tools, formal methods are now also being applied to application domains that are not inherently safety critical in nature. We also found out that it is not possible to generate a matrix that renders the selection of the right formal method an automatic process. Our research shows that besides technical grounds (eg, modeling capabilities and supported development phases), formal methods should also be evaluated from social and industrial perspectives. The criteria were then evaluated on several model-oriented state-based formal methods. The criteria were chosen through a literature review, discussions with experts from academia and practitioners from industry, and decade-long personal experience with the application of formal methods in industrial and academic projects.
In this paper, we present the criteria for evaluating and comparing different formal methods. However, one thing that is still missing is the evaluation criteria that help software practitioners choose the right formal method for the problem at hand. After a number of success stories in safety-critical domains, we are starting to witness applications of formal methods in contemporary systems and software engineering.
0 kommentar(er)
