Extending the scope of modular analysis for the validation of large systems

计算机系统日益复杂，对验证和确认有严重影响，特别是对关键系统(如医疗监督、航空电子任务系统)。标准方法是建立系统的正式模型，并自动分析其行为。这样的模型可以用模块化的高级描述来捕获，但状态的数量通常如此之大，以至于无法进行分析。本项目中提出的模块化分析将分析技术与模型的结构相匹配。初步结果是有希望的，并激励该技术扩展到更大类别的模块化描述。

The increasing complexity of computer systems has severe implications for verification and validation, especially for critical systems (e.g. medical supervision, avionics mission systems). The standard approach is to build a formal model of the system and automatically analyse its behaviour. Such models can be captured in a modular, high-level description, but the number of states is usually so large as to preclude analysis. The modular analysis proposed in this project matches the analysis technique to the structure of the model. Preliminary results are promising and motivate the extension of the technique to a larger class of modular descriptions.