245:
Formal specification techniques have existed in various domains and on various scales for quite some time. Implementations of formal specifications will differ depending on what kind of system they are attempting to model, how they are applied and at what point in the software life cycle they have
152:
concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifier's understanding of the specification and its relationship with the underlying problem domain. If not, the specification probably needs to be changed to better reflect the domain
51:
In each passing decade, computer systems have become increasingly more powerful and, as a result, they have become more impactful to society. Because of this, better techniques are needed to assist in the design and implementation of reliable software. Established engineering disciplines use
139:
A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification”. Whether the formal specification correctly describes the problem to be solved is a separate issue. It is also a difficult issue to address since it
38:
are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These
325:
In addition to the above paradigms, there are ways to apply certain heuristics to help improve the creation of these specifications. The paper referenced here best discusses heuristics to use when designing a specification. They do so by applying a
176:
that focus on flexibility. Doing a formal specification of the whole system up front is often perceived as being the opposite of flexible. However, there is some research into the benefits of using formal specifications with "agile"
156:
Formal methods of software development are not widely used in industry. Most companies do not consider it cost-effective to apply them in their software development processes. This may be for a variety of reasons, some of which are:
709:
Nummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 August 2011). "Supporting agile development by facilitating natural user interaction with executable formal specifications".
52:
mathematical analysis as the foundation of creating and validating product design. Formal specifications are one such way to achieve this in software engineering reliability as once predicted. Other methods such as
76:
with respect to its specification. This allows incorrect system designs to be revised before any major investments have been made into an actual implementation. Another approach is to use probably correct
316:
351:
754:
Proceedings of the 2002 Annual
Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology
131:
on software implementations. These proofs may be used to validate a specification, verify correctness of design, or to prove that a program satisfies a specification.
188:
A solution to this would be to develop tools and models that allow for these techniques to be implemented but hide the underlying mathematics
107:
A good specification must have some of the following attributes: adequate, internally consistent, unambiguous, complete, satisfied, minimal.
386:
43:
in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.
826:
796:
571:
17:
211:
This is not entirely true, by limiting their use to only core parts of critical systems they have shown to be cost-effective
197:
676:
641:
460:
411:
185:
They require a high level of mathematical expertise and the analytical skills to understand and apply them effectively
761:
487:
81:
steps to transform a specification into a design, which is ultimately transformed into an implementation that is
73:
816:
141:
327:
127:
One of the main reasons there is interest in formal specifications is that they will provide an ability to
145:
672:
381:
173:
140:
ultimately concerns the problem constructing abstracted formal representations of an informal concrete
246:
been introduced. These types of models can be categorized into the following specification paradigms:
445:
406:
347:
275:
128:
514:
821:
435:
777:
509:
455:
343:
231:
500:
362:
area, formal specification is often used to describe non-functional properties (Web services
450:
144:, and such an abstraction step is not amenable to formal proof. However, it is possible to
8:
69:
727:
647:
577:
527:
363:
78:
757:
637:
567:
153:
understanding of those involved with producing (and implementing) the specification.
581:
531:
731:
719:
708:
651:
629:
559:
519:
296:
languages such as
Statecharts, PROMELA, STeP-SPL, RSML or SCR rely on this paradigm
53:
31:
749:
800:
792:
491:
483:
440:
93:
626:
Proceedings of the conference on the future of
Software engineering - ICSE '00
810:
563:
495:
65:
723:
523:
203:
They do not do a good job of specifying user interfaces and user interaction
750:"What design heuristics may enhance the utility of a formal specification?"
376:
359:
633:
396:
339:
271:
416:
556:
Proceedings of 16th
International Conference on Software Engineering
401:
355:
279:
149:
290:
behavior based on transitions from state-to-state of the system
481:
421:
346:. Others include the Specification Language (VDM-SL) of the
319:, GIST, Petri nets or process algebras rely on this paradigm
92:
an implementation, but rather it may be used to develop an
498:(2009). "Using formal specifications to support testing".
267:
series of sequential steps, (e.g. a financial transaction)
554:
Gaudel, M.-C. (1994). "Formal specification techniques".
490:; Kapoor, K.; Krause, P.; LĂĽttgen, G.; Simons, A. J. H.;
304:
specify a system as a structure of mathematical functions
307:
OBJ, ASL, PLUSS, LARCH, HOL or PVS rely on this paradigm
747:
486:; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.;
88:
It is important to note that a formal specification is
164:
High initial start up cost with low measurable returns
619:
617:
615:
613:
611:
609:
607:
605:
603:
601:
599:
597:
595:
593:
591:
667:
665:
663:
661:
196:They do not capture properties of interest for all
704:
702:
700:
624:Lamsweerde, A. V. (2000). "Formal specification".
72:techniques to demonstrate that a system design is
743:
741:
588:
808:
658:
114:Constructability, manageability and evolvability
56:are more commonly used to enhance code quality.
697:
738:
549:
547:
545:
543:
541:
793:A Case for Formal Specification (Technology)
477:
475:
748:van der Poll, John A.; Paula Kotze (2002).
671:
623:
538:
513:
472:
148:a specification by proving “challenge”
14:
809:
712:ACM SIGSOFT Software Engineering Notes
553:
256:assertions are interpreted over time
24:
461:Specification (technical standard)
342:is an example of a leading formal
253:behavior based on system histories
25:
838:
785:
333:
96:. Formal specifications describe
293:best used with a reactive system
172:A lot of software companies use
110:A good specification will have:
287:Transition-based specification
264:behavior based on system states
123:Powerful and efficient analysis
827:Formal specification languages
770:
482:Hierons, R. M.; Bogdanov, K.;
134:
13:
1:
466:
46:
250:History-based specification
240:
7:
429:
10:
843:
312:Operational Specification
261:State-based specification
27:Aspect of computer science
446:Model-based specification
352:Abstract Machine Notation
348:Vienna Development Method
301:Functional specification
104:the system should do it.
776:S-Cube Knowledge Model:
756:. SAICSIT '02: 179–194.
564:10.1109/ICSE.1994.296781
315:early languages such as
100:a system should do, not
68:, it is possible to use
724:10.1145/1988997.2003643
524:10.1145/1459352.1459354
436:Algebraic specification
83:correct by construction
59:
677:"Formal Specification"
456:Specification language
344:specification language
232:separation of concerns
803:by Coryoth 2005-07-30
634:10.1145/336512.336546
501:ACM Computing Surveys
282:rely on this paradigm
36:formal specifications
18:Program specification
817:Formal specification
778:Formal Specification
684:Software Engineering
628:. pp. 147–159.
558:. pp. 223–227.
451:Software engineering
224:Low-level ontologies
494:; Woodward, M. R.;
217:Other limitations:
208:Not cost-effective
174:agile methodologies
70:formal verification
39:specifications are
799:2005-10-21 at the
364:quality of service
328:divide-and-conquer
270:languages such as
236:Poor tool feedback
573:978-0-8186-5855-6
369:Some tools are:
16:(Redirected from
834:
780:
774:
768:
767:
745:
736:
735:
706:
695:
694:
692:
690:
681:
673:Sommerville, Ian
669:
656:
655:
621:
586:
585:
551:
536:
535:
517:
479:
32:computer science
21:
842:
841:
837:
836:
835:
833:
832:
831:
807:
806:
801:Wayback Machine
788:
783:
775:
771:
764:
746:
739:
707:
698:
688:
686:
679:
670:
659:
644:
622:
589:
574:
552:
539:
515:10.1.1.144.3320
492:Vilkomir, S. A.
480:
473:
469:
432:
336:
243:
137:
120:Communicability
62:
49:
28:
23:
22:
15:
12:
11:
5:
840:
830:
829:
824:
822:Formal methods
819:
805:
804:
787:
786:External links
784:
782:
781:
769:
762:
737:
696:
657:
643:978-1581132533
642:
587:
572:
537:
470:
468:
465:
464:
463:
458:
453:
448:
443:
441:Formal methods
438:
431:
428:
427:
426:
425:
424:
419:
414:
409:
404:
399:
391:
390:
389:
384:
379:
335:
334:Software tools
332:
323:
322:
321:
320:
310:
309:
308:
305:
299:
298:
297:
294:
291:
285:
284:
283:
268:
265:
259:
258:
257:
254:
242:
239:
238:
237:
234:
228:
225:
222:
215:
214:
213:
212:
206:
205:
204:
201:
200:in the project
193:Limited scope
191:
190:
189:
186:
180:
179:
178:
167:
166:
165:
142:problem domain
136:
133:
129:perform proofs
125:
124:
121:
118:
115:
94:implementation
61:
58:
48:
45:
26:
9:
6:
4:
3:
2:
839:
828:
825:
823:
820:
818:
815:
814:
812:
802:
798:
795:
794:
790:
789:
779:
773:
765:
763:9781581135961
759:
755:
751:
744:
742:
733:
729:
725:
721:
717:
713:
705:
703:
701:
685:
678:
674:
668:
666:
664:
662:
653:
649:
645:
639:
635:
631:
627:
620:
618:
616:
614:
612:
610:
608:
606:
604:
602:
600:
598:
596:
594:
592:
583:
579:
575:
569:
565:
561:
557:
550:
548:
546:
544:
542:
533:
529:
525:
521:
516:
511:
507:
503:
502:
497:
493:
489:
485:
478:
476:
471:
462:
459:
457:
454:
452:
449:
447:
444:
442:
439:
437:
434:
433:
423:
420:
418:
415:
413:
410:
408:
405:
403:
400:
398:
395:
394:
392:
388:
385:
383:
380:
378:
375:
374:
372:
371:
370:
367:
365:
361:
357:
354:(AMN) of the
353:
349:
345:
341:
331:
329:
318:
314:
313:
311:
306:
303:
302:
300:
295:
292:
289:
288:
286:
281:
277:
273:
269:
266:
263:
262:
260:
255:
252:
251:
249:
248:
247:
235:
233:
229:
227:Poor guidance
226:
223:
220:
219:
218:
210:
209:
207:
202:
199:
195:
194:
192:
187:
184:
183:
181:
175:
171:
170:
168:
163:
162:
160:
159:
158:
154:
151:
147:
143:
132:
130:
122:
119:
116:
113:
112:
111:
108:
105:
103:
99:
95:
91:
86:
84:
80:
75:
71:
67:
66:specification
64:Given such a
57:
55:
44:
42:
37:
33:
19:
791:
772:
753:
715:
711:
687:. Retrieved
683:
625:
555:
505:
499:
484:Bowen, J. P.
393:Model-based
368:
360:Web services
337:
324:
244:
216:
198:stakeholders
169:Flexibility
155:
138:
126:
109:
106:
101:
97:
89:
87:
82:
63:
50:
40:
35:
29:
718:(4): 1–10.
182:Complexity
177:development
135:Limitations
811:Categories
689:3 February
488:Harman, M.
467:References
417:Petri Nets
373:Algebraic
340:Z notation
330:approach.
79:refinement
47:Motivation
510:CiteSeerX
496:Zedan, H.
358:. In the
241:Paradigms
221:Isolation
117:Usability
797:Archived
675:(2009).
582:60740848
532:10686134
508:(2): 1.
430:See also
356:B-Method
350:and the
150:theorems
146:validate
732:2139235
652:4657483
317:Paisley
74:correct
54:testing
760:
730:
650:
640:
580:
570:
530:
512:
41:formal
728:S2CID
680:(PDF)
648:S2CID
578:S2CID
528:S2CID
387:Lotos
377:Larch
230:Poor
161:Time
758:ISBN
691:2013
638:ISBN
568:ISBN
422:TLA+
338:The
98:what
60:Uses
720:doi
630:doi
560:doi
520:doi
412:CSP
407:VDM
382:OBJ
366:).
278:or
276:VDM
102:how
90:not
30:In
813::
752:.
740:^
726:.
716:36
714:.
699:^
682:.
660:^
646:.
636:.
590:^
576:.
566:.
540:^
526:.
518:.
506:41
504:.
474:^
274:,
85:.
34:,
766:.
734:.
722::
693:.
654:.
632::
584:.
562::
534:.
522::
402:B
397:Z
280:B
272:Z
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.