带时间和资源约束的实例化过程模型验证方法

软件过程的性能是由软件过程模型和软件过程实例化两方面因素决定，如果对软件过程进行了不恰当的实例化，会导致成本超支、进度延期、甚至项目失败．已有的过程描述法不足以分析实例化过程模型，由于没有考虑实例化阶段的时间资源约束，语法结构正确的过程模型并不能保证过程执行的正确性．提出一种带时间和资源约束的实例化过程模型验证方法，为目前已有的s-TRISO／ML建模语言增加时间和资源约束属性，然后提出了从s-TRISO／ML模型转换成时间自动机的转换方法和实现算法，利用已有的分析工具Uppaal对转换得到的时间自动机的性质进行验证，得到一个合理的实例化模型，从而为真实的开发流程提供指导．

Approach to Verify the Process Instantiation Model with Time and Resource Constraints

The performance of software process is related with the software process models and the resource allocations of software processes. If a correct model is impertinently allocated with the limited resource of a software organization, as a result, the performance of the software process may fail to reach the actual requirement, followed by delay, over-cost, and even failure. The existing approach based on process automata isn't fit for the analysis of instantiation model. A model with only correct structure can't ensure a successful enactment, because it lacks schedule information. This paper presents an approach to verify the process instantiation model with time and resource constraints, which is an extension of existing s-TRISO/ML process modeling language. This paper also presents an approach to convert from an s-TRISO/ML model into timed automata and explains converting algorithm. Finally, making use of UPPAAL to carry out the function verification on the converted timed automata, we can get a reasonable instantiation model to provide guidance for the actual process development.