Specifiche basate sul modello - Model-based specification
La specifica basata sul modello è un approccio alla specifica formale in cui la specifica del sistema è espressa come un modello di stato del sistema . Questo modello di stato è costruito utilizzando entità matematiche ben comprese come insiemi e funzioni . Le operazioni di sistema vengono specificate definendo come influenzano lo stato del modello di sistema.
Le notazioni più utilizzate per lo sviluppo di specifiche basate su modello sono VDM e Z (pronunciato Zed, non Zee). Queste notazioni sono basate sulla teoria degli insiemi tipizzati . I sistemi sono quindi modellati utilizzando insiemi e relazioni tra insiemi.
Un altro approccio ben noto alla specificazione formale è la specificazione algebrica .
