Formal methods and tools are a popular means of analysing the correctness properties of computer network protocols, such as safety, liveness and security. First the protocol under scrutiny is described in a formal language, which often results in a more precise definition of its function. Subsequently, the properties to be analysed are specified in a suitable logic. Finally, to decide whether or not the protocol fulfils certain properties, automatic tools are used to analyse it. The outcome either proves the protocol to be correct with respect to the relevant properties or shows there to be a problem.
Formal modelling and verification in service-oriented computing
Ter Beek M H;Gnesi S;Martinelli F;Mazzanti F;Petrocchi M
2007
Abstract
Formal methods and tools are a popular means of analysing the correctness properties of computer network protocols, such as safety, liveness and security. First the protocol under scrutiny is described in a formal language, which often results in a more precise definition of its function. Subsequently, the properties to be analysed are specified in a suitable logic. Finally, to decide whether or not the protocol fulfils certain properties, automatic tools are used to analyse it. The outcome either proves the protocol to be correct with respect to the relevant properties or shows there to be a problem.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
prod_68406-doc_130569.pdf
accesso aperto
Descrizione: Formal modelling and verification in service-oriented computing
Tipologia:
Versione Editoriale (PDF)
Dimensione
187.44 kB
Formato
Adobe PDF
|
187.44 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.