M. Verdicchio and P. San Pietro (Italy)
This work aims at supporting the implementation of a secure distributed system from a model-checked abstract model, while preserving its verified safety properties.We choose the Secure Electronic Transaction protocol as an example to be implemented in Java. On the basis of the protocol specifications, an abstract model is created as a fi nite state machine and verified by means of the SPIN model checker. We illustrate a safety preserving translation pro cess that aims at enabling programmers to implement the protocol as a secure Java distributed program.
Important Links:
Go Back
