olemus
ISO/IEC 2382:
spetsifikatsioon, mis on
kirjutatud formaalses notatsioonis,
sageli õigsuse tõestamiseks
= specification written in a formal notation, often for use in correctness proving

ISO/IEC 2382, ISO/IEC/IEEE 24765:
spetsifikatsioon teostuse kõlblikkuse
matemaatiliseks tõestuseks või
teostuse matemaatiliseks tuletamiseks
= specification that is used to prove mathematically the validity of an implementation or to derive mathematically the implementation

ISO/IEC/IEEE 24765:
spetsifikatsioon, mis on koostatud ja kinnitatud
kehtivate standardite järgi
= specification written and approved in accordance with established standards

ülevaade
https://en.wikipedia.org/wiki/Formal_specification

näiteid
http://cgi.csc.liv.ac.uk/~coopes/comp201/handouts/SE_L11.pdf

https://hal.inria.fr/inria-00507300/file/FormalSpecificationandValidationofSecurityPolicies.pdf

https://formal.iti.kit.edu/beckert/pub/csduml2004.pdf

https://ifs.host.cs.st-andrews.ac.uk/Books/SE9/WebChapters/PDF/Ch_27_Formal_spec.pdf

https://lamport.azurewebsites.net/pubs/wsfm-web.pdf

https://www.iso.org/obp/ui/#iso:std:iso-iec:13568:ed-1:v1:en

https://www.ifi.uzh.ch/dam/jcr:a39169f2-dc62-4507-ab8a-de35942fb09b/RE_I_Slides_Part_II_10-13.pdf

vt ka
- formaalne kirjeldus
- formaalne meetod
- formaalne mudel