位置：立项数据库 > 立项详情页
组合Web服务的建模与验证
  • 项目名称：组合Web服务的建模与验证
  • 项目类别：面上项目
  • 批准号：60873018
  • 申请代码：F020106
  • 项目来源：国家自然科学基金
  • 研究期限：2009-01-01-2011-12-31
  • 项目负责人：段振华
  • 负责人职称：教授
  • 依托单位：西安电子科技大学
  • 批准年度：2008
中文摘要：

以投影时序逻辑的可执行子集Framed Tempura 为基础，定义组合Web 服务建模语言WS-Tempura 的语句结构和通信机制，研究该语言的操作语义，并开发该语言的解释器。研究该语言的正则形及正则图，研究该语言的可判定性，判定算法及算法复杂度。研究BPEL 流程到WS-Tempura 程序的转换规则，并开发自动转换工具，以实现BPEL 流程模型的自动提取。研究基于WS-Tempura 程序执行的仿真和错误诊断技术；基于执行生成的正则图，研究该图的性质以及相关的程序分析技术。以WS-Tempura 建模语言描述组合Web 服务的行为，以PPTL 描述组合Web 服务的性质，研究基于模型检测工具SPIN 的验证方法；同时，在由WS-Tempura 和PPTL 组成的统一时序逻辑框架下，研究基于SAT 的模型、性质一体化的组合Web 服务验证方法。

中文主题词： 组合Web 服务；模型检测；投影时序逻辑；仿真；验证
结论摘要：

英文主题词web service composition;model checking;projection temporal logic(PTL);simulation;verification

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 43
  • 21
  • 2
  • 0
  • 2
期刊论文
基于枢轴选择策略的多核并行skyline 算法
支持stutter-不变性的命题区间时序逻辑
面向命题投影时序逻辑的安全协议模型检测
一种采用预排序策略的多核并行skyline算法
利用投影时序逻辑的多内核进程调度建模与验证
Model Checking Interval Temporal Logic
Unconditional Secure Communication: a Russian Cards Protocol
框架时序逻辑语言MSVL中面向对象机制的实现
Axiomatic Semantics of Projection Temporal Logic Programs
PPTL模型检测器实现的一个关键技术
基于投影时序逻辑的Web服务模型检测
Complexity of Propositional Projection Temporal Logic with Star
基于命题投影时序逻辑的单调速率调度算法模型检测
MSVL语言的公理系统的程序验证
动态Web服务组合的选择策略
面向对象的时序逻辑语言
Operational Semantics of Framed Tempura
国际Petri网理论与应用最新研究进展
着色Petri网模型检测工具的扩展及其在Web服务组合中的应用
有穷时间投影时序逻辑的完备公理系统
投影时序逻辑在系统建模中的应用
基于事件确定有限自动机的UML2．0序列图描述与验证
BPEL流程建模中的交叠模式分析与转换
基于UML2.0的软件安全测试方法
Symbolic Algorithmic Analysis of Rectangular Hybrid Systems
会议论文
An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems
Non-Functional Requirements Elicitation and Incorporation into Class Diagrams
Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic
Alternating Interval Based Temporal Logics
A Model-driven Approach for Dynamic Web Service Composition
UML Statecharts' PTL Formal Semantics
A Model-driven Approach for Generating Business Processes and Process Interaction Semantics
A Proof System for Projection Temporal Logic
Verification of Use Case with Petri Nets in Requirement Analysis
Verification of Hardware Designs: A Case Study
Model Checking Multirate Hybrid System with Restricted Convex Polyhedron
Making Abstraction Refinement Efficient in Model Checking
A Semantic Model for Many-core Parallel Computing
A Transformation From PPTL to S1S
Generalized Russian Cards Problem
An Executable Concurrent Model for OWL-S Process Models
An Improved Decision Procedure for Propositional Projection Temporal Logics with Star
Specification and Verification of UML2.0 Sequence Diagrams using Event Deterministic Finite Automata
Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates
Public Communication Based on Russian Cards Protocol: A Case Study
ESHMP: A Stall-Timed-Based Scheduling for Performance Heterogenous Muticore Systems
专利
基于非结构化P2P网络的搜索方法
基于扫描方法的查找FPGA芯片空白区域的方法
著作
2008 8th International Conference on Application of Concurrency to System Design, ACSD 2008, Proceedings
Theory and Applications of Models of Computation - 5th International Conference, TAMC 2008, Proceedings
相关项目
航站楼人群应急疏散微观仿真模型研究
期刊论文 9 会议论文 2
环路热管(Loop Heat Pipe)两相传热机理的理论与实验研究
期刊论文 13 会议论文 4
基于高阶逻辑的分数阶建模与验证理论研究
期刊论文 26 会议论文 4 获奖 6 著作 1
包封法及推理系统的可判定性
期刊论文 7 会议论文 2 著作 2
基于ABMS的电子商务治理仿真系统及其应用研究
期刊论文 7 会议论文 2 著作 1
水环境质变的非确定人为-自然协同要素仿真
期刊论文 21 会议论文 5
车路协同系统多分辨率建模与仿真方法研究
期刊论文 16 会议论文 16 获奖 2
电力市场稳定性与电力系统稳定性的相互影响
期刊论文 3 会议论文 2
提速机车车辆横向非线性振动的理论与试验研究
期刊论文 15 会议论文 1 获奖 2 著作 1
段振华的项目
C/Verilog程序的MSVL验证理论与方法
期刊论文 3
开放软件系统的基础理论与关键技术
期刊论文 20
基于FPGA的高可信嵌入式系统的基础研究
期刊论文 15 会议论文 9
基于语义的恶意程序主动防御与检测机理研究
期刊论文 7
混合系统的形式验证
期刊论文 11 会议论文 21 获奖 1 著作 3
框架时序逻辑程序设计
期刊论文 54 会议论文 46 获奖 1 著作 3
第29届国际Petri网理论与应用大会
第5届计算模型理论与应用国际会议
构造可信、高效软件系统的基础研究
期刊论文 8