Research On The Combined Modeling And Verification For Component-based Systems

AADL is a kind of language for architecture modeling of embedded real-time system.Because of its modeling contains both software and hardware,it is widely used in many security critical systems such as the avionics system and the large component-based system.For the established model of the system,how to verify its security and reliability has become a main direction in the field of AADL research.AADL specification describe the semantics of the thread,process,the behavior annex,connection for the large system which uses component combination technology to realize packing multi-service function,but for the states and states with the data constraints description is slightly less than,while we know the Z language in the data constraint description has a significant role and the computation tree logic can give a full description of the temporal properties during the transitions between states.We expand AADL with Z language and CTL,so that the model of the subsystems of the huge system can be better combined into a safe and reliable model.In the respect of formal modeling,we propose to expand the AADL‘s behavior annex with the Z language and the computation tree logic to describe the data constraint and the temporal properties of the transitions between states,and then we propose the Z-AADL modeling specification which enhances the flexibility and diversity of AADL modeling and provides the possibility to adopt different modeling types for different developers.Besides,we propose a combined verification which combines model checking and theorem proving to verify the combined model of the component-based system.The model checking part,we convert the Z-AADL modeling specification to the ZIA specification and then verify the security and reliability of the huge component-based system.The theorem proving part,we first give the axiom system of the computation tree logic and then use the theorem proving PVS to verify the temporal logic formulas,so as to verify the security and reliability of the whole system in the temporal property.We give the examples to illustrate the practicability of the proposed modeling and verification methods at the end of each chapter.