嵌入式实时系统多数应用在安全性要求较高的场合,因此需要保证系统的正确性。复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质。时间Petri网是有严格数学基础的图形表达工具,适合对实时系统建模...嵌入式实时系统多数应用在安全性要求较高的场合,因此需要保证系统的正确性。复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质。时间Petri网是有严格数学基础的图形表达工具,适合对实时系统建模;时间自动机(Timed Automata,TA)有成熟的验证工具,被广泛用于实时系统的模型检验和验证。本文提出一种基于着色时间Petri网(Colored Time Petri Net,CTPN)的实时系统的验证方法,用CTPN对带有控制流和数据流的实时系统建模,通过转换规则将CTPN模型转换成语义等价的TA模型,利用模型检验工具UPPAAL验证系统的性质。最后,用实例证明此方法有效。展开更多
在面向服务的环境中,服务组合的可执行能力具有很大的不确定性,在业务级别组合服务更是如此。影响业务级服务组合可执行能力的因素是多方面的,本文针对组合的服务的逻辑结构和业务服务到具体服务的匹配方法对业务级服务组合可执行能力...在面向服务的环境中,服务组合的可执行能力具有很大的不确定性,在业务级别组合服务更是如此。影响业务级服务组合可执行能力的因素是多方面的,本文针对组合的服务的逻辑结构和业务服务到具体服务的匹配方法对业务级服务组合可执行能力的影响,提出了一种基于着色时间 Petri 网(CTPN)的业务级服务组合可执行能力验证方法,并以制造业网格应用平台 AmGrid 为案例,展示了该方法在平台中的应用效果。展开更多
提出一种定量评价C4ISR(Command Control Communication Computer Intelligence Surveillance and Reconnaissance)系统任务实时性方法——时序着色模糊时间Petri网(TCFTPN)方法。用时序逻辑公式来限制着色Petri网的变迁引发行为,用模...提出一种定量评价C4ISR(Command Control Communication Computer Intelligence Surveillance and Reconnaissance)系统任务实时性方法——时序着色模糊时间Petri网(TCFTPN)方法。用时序逻辑公式来限制着色Petri网的变迁引发行为,用模糊时间来表示各工作过程的时延特性和降级工作问题。通过估计在规定的时间内标识从任务开始状态到达任务完成状态的概率来确定C4ISR系统的任务实时性。展开更多
文摘嵌入式实时系统多数应用在安全性要求较高的场合,因此需要保证系统的正确性。复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质。时间Petri网是有严格数学基础的图形表达工具,适合对实时系统建模;时间自动机(Timed Automata,TA)有成熟的验证工具,被广泛用于实时系统的模型检验和验证。本文提出一种基于着色时间Petri网(Colored Time Petri Net,CTPN)的实时系统的验证方法,用CTPN对带有控制流和数据流的实时系统建模,通过转换规则将CTPN模型转换成语义等价的TA模型,利用模型检验工具UPPAAL验证系统的性质。最后,用实例证明此方法有效。
文摘在面向服务的环境中,服务组合的可执行能力具有很大的不确定性,在业务级别组合服务更是如此。影响业务级服务组合可执行能力的因素是多方面的,本文针对组合的服务的逻辑结构和业务服务到具体服务的匹配方法对业务级服务组合可执行能力的影响,提出了一种基于着色时间 Petri 网(CTPN)的业务级服务组合可执行能力验证方法,并以制造业网格应用平台 AmGrid 为案例,展示了该方法在平台中的应用效果。
文摘提出一种定量评价C4ISR(Command Control Communication Computer Intelligence Surveillance and Reconnaissance)系统任务实时性方法——时序着色模糊时间Petri网(TCFTPN)方法。用时序逻辑公式来限制着色Petri网的变迁引发行为,用模糊时间来表示各工作过程的时延特性和降级工作问题。通过估计在规定的时间内标识从任务开始状态到达任务完成状态的概率来确定C4ISR系统的任务实时性。
