摘要：针对编制方式生成的组合Web服务需要用一个工作流引擎执行这个特征,对投影时序逻辑进行了扩展,并用扩展投影时序逻辑描述和验证组合Web服务.将组合Web服务视为一个基于过程的工作流,将工作流引擎与组合Web服务组成部分的一次不可分割的消息交互抽象为一个原子过程.用扩展投影时序逻辑公式描述原子过程,用扩展投影时序逻辑操作符定义过程组合规则、连接过程描述公式,得到组合Web服务描述公式.通过模拟组合Web执行,可验证组合Web服务满足系统的需求和性质,为提高组合Web服务设计的可靠性提供了依据.

摘要：投影时序逻辑是一种具有离散时间模型的时序逻辑,其部分子集又是一种程序设计语言,可处理顺序和并发计算.文章讨论应用投影时序逻辑对数字系统进行形式描述和验证的方法,该方法可在数字系统的不同层级设计过程中,使用投影时序逻辑对其系统行为和性质进行形式化的描述及验证,从而提高系统设计的可信性.

摘要：本文讨论从状态图到PTL形式规范的转化方法.状态图是描述系统行为的半形式化的图形工具,但缺少精确的形式语义,PTL(投影时序逻辑)是一种具有离散的时间模型的时序逻辑,把状态图转换到PTL后可以使其具有精确的形式语义并能使用形式化验证方法来证明状态图所描述的系统的一些重要性质是否得到满足,同时可把系统的形式描述转换为Tempura程序进行模拟,从而提高系统设计的可信性.

摘要：本文提出对寄存器传送语言(RTL)描述的数字系统运用投影时序逻辑进行形式化描述并验证的方法。通过使用投影时序逻辑对RTL的形式语义进行定义,可把一个用寄存器传输语言描述的系统转换成投影时序逻辑的公式,从而使用投影时序逻辑可执行子集MSVL对系统行为和性质进行形式化的描述及验证,提高系统设计的可信性。

摘要：随着Web服务应用的迅速发展,Web服务提供方的安全问题已成为制约其实际应用的主要障碍之一。文中着重讨论了Web服务提供方面临的安全问题,引入了一种基于安全策略与实现分离的信息安全解决模型,并根据Web服务的实际情况进行了改进,方便了Web服务提供方动态地制定安全策略、灵活地实现策略指导下的各种安全措施。最后,采用投影时序逻辑(PTL,Projection Temporal Logic)形式化描述了该模型中资源访问决策部分的规范说明。