Author: Miguel Ferreira
This is a Specification of the File System Layer, sliced at the
FS_DeleteFileDir operation, as defined in the INTEL Flash File
System document. It includes: a VDM++ model that can be model
checked in an equivalent Alloy model; and an adapted version
of the VDM++ model to be used in the Overture Automated Proof
Support system. In the test class UseFileSystemLayerAlg there
are a few examples of using the traces primitives used for
test automation. This model has been developed by Miguel
Ferreira
Language Version: vdm10
Entry point : new UseFileSystemLayerAlg().dummy()
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|