S A Deloach,T C Hartrum.A theory-based representation for object-oriented domain models[J].IEEE Trans.on Software Engineering,2000,26(6).
[2]
S Owre,J Rushby,N Shankar,F V Henke.Formal verification for fault-tolerant architectures:Prolegomena to the design of PVS[J].IEEE Trans.on Software Engineering,1995,21(2):107-125.
William Chan,Richard J Anderson,et al.Model checking large software specification[J].IEEE Trans.on Software Engineering,1998,24(7):498-520.
[5]
Diego Latella,Istvan Majzik,Mieke Massink.Automatic verification of a behavioral subset of UML statechart diagrams using the SPIN model-checker[J].Formal aspects of computing,1999,11:637-664.
