We present two generic formal security models for operating systems of multiapplicative smart cards. The models formalize the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applica

Although formal methods have been successfully applied in various industrial applications, their use in software development is still restricted to individual case studies. To overcome this situation we aim at a methodology for an evolutionary formal software development which allows for a stepwise and incremental development process along the line of rapid prototyping. The approach is based on work on a formal management of change for formal developments which is able to maintain proofs when changing specifications.