Start line:  
End line:  

Snippet Preview

Snippet HTML Code

Stack Overflow Questions
This example is for a trusted gateway made by John Fitzgerald and 
Peter Gorm Larsen inspired by a more comprehensive model developed
by British Aerospace. THe work undertaken here was published in:

* Peter Gorm Larsen, Tom Brookes, Mike Green and John Fitzgerald, 
A Comparison of the Conventional and Formal Design of a Secure System 
Component, Nordic Seminar on Dependable Computing Systems, August, 1994.

* J.S. Fitzgerald, T.M. Brookes, M.A. Green, and P.G. Larsen, Formal 
and Informal Specifications of a Secure System Component: first results 
in a comparative study, Formal Methods Europe'94 - : Industrial Benefit
of Formal Methods, Springer Verlag, October 1994.

* Peter Gorm Larsen, John Fitzgerald, Tom Brookes, Mike Green, Formal 
Modelling and Simulation in the Development of a Security-critical 
Message Processing System, Anglo-French workshop on Formal Methods, 
Modelling and Simulation for System Engineering, Saint-Quentin, 
France, February, 1995.

* John Fitzgerald, Peter Gorm Larsen, Tom Brookes and Mike Green, 
Developing a Security-critical System using Formal and Conventional 
Methods, Chapter 14 in “Applications of Formal Methods”, M.G. Hinchey 
and J.P. Bowen (editors), Prentice Hall International Series in 
Computer Science, September 1995.

* Peter Gorm Larsen, John Fitzgerald and Tom Brookes, Lessons Learned 
from Applying Formal Specification in Industry, IEEE Software, 
pp 48-56, May 1996.

* T.M. Brookes, J.S. Fitzgerald, and P.G. Larsen, Formal and Informal 
Specifications of a Secure System Component: final results in a 
comparative study, “Formal Methods Europe'96”, pp 214-227, Springer 
Verlag, March 1996.

#******************************************************
#  AUTOMATED TEST SETTINGS
#------------------------------------------------------
#AUTHOR= John Fitzgerald and Peter Gorm Larsen
#LANGUAGE_VERSION=classic
#INV_CHECKS=true
#POST_CHECKS=true
#PRE_CHECKS=true
#DYNAMIC_TYPE_CHECKS=true
#SUPPRESS_WARNINGS=false
#ENTRY_POINT=DEFAULT`Occurs("topsecret","peter87topsecrethere next")
#EXPECTED_RESULT=NO_ERROR_TYPE_CHECK
#******************************************************
New to GrepCode? Check out our FAQ X