An Integrated Formalized Model and Its Operational Semantics

Guofang Kuang · Luoyang Shifan Xueyuan xuebao · 2011

Formal methods play an important role in the study of program verification and model-checking.Integrated formal methods are a development direction of formal methods.The model of BCCS which integrates B language and CCS is a hybrid model and in this model,a light-weight description language is provided.In order to ensure the completeness and consistency of this language,the operational semantics of BCCS is given on the basis of operational semantics of value-passing CCS and by combining the definition of Abstract data structure,the systems restrictions and functional treatment using the B method so as to present a further description of the model of BCCS.

Read the paper · More papers on PaperTik