【61133001】开放软件系统的基础理论与关键技术国家自然基金项目

开放软件系统的基础理论与关键技术

项目批准号： 61133001

批准年份： 2011

学科分类： F0203.软件理论、软件工程与服务

项目负责人：段振华

资助类别：重点项目

负责人职称：教授

依托单位：西安电子科技大学

资助金额： 270万元

关键词：验证;模型驱动;开放软件系统;测试;仿真

起止时间： 2012-01-01到2016-12-31

中英文摘要
结题摘要
结题报告
项目成果
项目参与人

查看更多信息请先登录或注册

序号	标题	类型	作者
1	Satisfiability of Linear Time Mu-Calculus on Finite Traces	会议论文	Cong Tian\|Cong Tian\|Bin Cui\|Bin Cui\|
2	An Extended π-calculus	会议论文	Ling Luo\|Zhenhua Duan\|
3	Effective Statistical Fault Localization Using Program Slices	会议论文	Yan Lei\|Xiaoguang Mao\|Ziying Dai\|Chengsong Wang\|
4	Modeling and Verification of an Interrupt System in μC/OS-III with TMSVL	会议论文	Cong Tian\|Cong Tian\|Nan Zhang\|Nan Zhang\|
5	A mechanism of function calls in MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
6	Linear time-dependent constraints programming with MSVL	期刊论文	Qian Ma\|Zhenhua Duan\|
7	Model Checking Multi-agent Systems with APTL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
8	真并发等价性下的流程模型转换方法	期刊论文	张曼\|段振华\|
9	Development of a Supporting Tool for Formalizing Software Requirements	会议论文	Xi Wang\|Shaoying Liu\|
10	Tissue Systems and Petri Net Synthesis	专著	Jetty Kleijn\|Maciej Koutny\|Marta Pietkiewicz-Koutny\|
11	LTLNFBA: make LTL translation more practical	会议论文	Jun Song\|Jun Song\|Zhenhua Duan\|Zhao Duan\|
12	Simulation of CTCS-3 protocol with temporal logic programming	会议论文	Peng Zhang\|Zhenhua Duan\|Cong Tian\|
13	Bounded Model Checking of MSVL Programs	会议论文	Bin Yu\|Zhenhua Duan\|Cong Tian\|
14	Bounded Model Checking of Traffic Light Control System	期刊论文	Bin Yu\|Zhenhua Duan\|Cong Tian\|
15	Model checking of C programs	会议论文	Yan Yu\|Zhenhua Duan\|
16	Building Requirements Traceability to Support Specification Construction and Evolution	会议论文	Weichen Cai\|Shaoying Liu\|
17	Effective fault localization approach using feedback	期刊论文	Yan Lei\|Xiaoguang Mao\|Ziying Dai\|Dengping Wei\|
18	A mechanism of function calls in MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
19	A Self-Organizing Trust Model Based on HP2P	会议论文	Yujiang Hui\|Yujiang Hui\|Cong Tian\|Cong Tian\|
20	二维逻辑PPTLSL的可满足性检查	期刊论文	段振华\|段振华\|田聪\|田聪\|
21	基于事件确定有限自动机的UML2.0序列图描述与验证	期刊论文	张琛\|段振华\|田聪\|
22	Design and Implementation of a Tool for Specifying Specification in SOFL	会议论文	Mo Li\|Shaoying Liu\|
23	A mechanism of function calls in MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
24	可信软件设计开发与验证的基础理论与关键技术	奖励	赵亮\|赵亮\|黄伯虎\|张琛\|
25	Zombie-city: A New Artificial Society Model	期刊论文	Mingsheng Tang\|Xinjun Mao\|Huiping Zhou\|
26	Model checking Petri nets with MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Mengchu Zhou\|Mengchu Zhou\|
27	A Method Based on MSVL for Verification of the Social Network Privacy Policy	会议论文	Xiaobing Wang\|Xiaobing Wang\|Tao Sun\|Tao Sun\|
28	Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic	期刊论文	Nan Zhang\|Zhenhua Duan\|
29	Formalizing and implementing types in msvl	会议论文	Xiaobing Wang\|Zhenhua Duan\|Liang Zhao\|
30	自由选择工作流网的可靠完备化简规则集	期刊论文	张曼\|段振华\|王小兵\|
31	A Memory Management Mechanism for MSVL	会议论文	Kai Yang\|Zhenhua Duan\|Cong Tian\|
32	BPEL流程建模中的交叠模式分析与转换	期刊论文	张曼\|段振华\|王小兵\|
33	Symbolic Model Checking for Alternating Projection Temporal Logic	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
34	Model Checking MSVL Programs Based on Dynamic Symbolic Execution	会议论文	Tian, Cong\|Cong Tian\|Zhang, Nan\|Nan Zhang\|
35	Modeling and Verification of RBC Handover Protocol	会议论文	Kai Yang\|Zhenhua Duan\|Cong Tian\|
36	A Taxonomy of Persistent and Nonviolent Steps	会议论文	Maciej Koutny\|Lukasz Mikulski\|Marta Pietkiewicz-Koutny\|
37	A Self-Organizing Trust Model Based on HP2P	会议论文	Yujiang Hui\|Yujiang Hui\|Cong Tian\|Cong Tian\|
38	A Practical Transformation from LTL to Automata	会议论文	Cong Tian\|Zhenhua Duan\|
39	An axiomatization for cylinder computation model	会议论文	Nan Zhang\|Zhenhua Duan\|Cong Tian\|
40	进位保留加法器的命题投影时序逻辑组合验证	期刊论文	张南\|段振华\|
41	LTLNFBA: making LTL translation more practical	会议论文	Jun Song\|Jun Song\|Zhenhua Duan\|Zhao Duan\|
42	Extending MSVL with Semaphore	会议论文	Xinfeng Shu\|Xinfeng Shu\|Zhenhua Duan\|Zhenhua Duan\|
43	NuTL2PFG:νTL公式的可满足性检查	期刊论文	段振华\|段振华\|田聪\|田聪\|
44	An approach to representing and utilizing specification pattern knowledge for computer-aided formalization of requirements	会议论文	Xi Wang\|Shaoying Liu\|
45	Model checking concurrent systems with MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
46	Runtime Veri？cation Monitor Construction for Three-valued PPTL	会议论文	Xiaobing Wang\|Dongmiao Liu\|Liang Zhao\|Yina Xue\|
47	基于CEGAR的C程序空指针解引用检测	期刊论文	段钊\|田聪\|段振华\|
48	An Efficient Approach for Abstraction Refinement in Model Checking	期刊论文	Cong Tian\|Zhenhua Duan\|
49	Symbolic Model Checking for Propositional Projection Temporal Logic	会议论文	Tao Pang\|Zhenhua Duan\|Cong Tian\|
50	Integration of Linear Constraints with a Temporal Logic Programming Language	会议论文	Qian Ma\|Zhenhua Duan\|Mengfei Yang\|
51	Automated Functional Scenarios-based Formal Specification Animation	会议论文	Mo Li\|Shaoying Liu\|
52	A cylinder computation model for many-core parallel computing	期刊论文	Nan Zhang\|Zhenhua Duan\|Cong Tian\|
53	A Formal Approach to Testing Programs in Practice	期刊论文	Shaoying Liu\|
54	Step semantics of boolean nets	期刊论文	Jetty Kleijn\|Maciej Koutny\|Marta Pietkiewicz-Ko\|
55	A structural transformation from p-π to MSV	期刊论文	Ling Luo\|Zhenhua Duan\|Cong Tian\|Xiaobing Wang\|
56	Model Checking μC/OS-III Multi-task System with TMSVL	会议论文	Nan Zhang\|Nan Zhang\|Conghao Zhou\|Conghao Zhou\|
57	Model Checking Multi-agent Systems with APTL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
58	Model checking open systems with alternating projection temporal logic	期刊论文	Cong Tian\|Cong Tian\|Zhenhua Duan\|Zhenhua Duan\|
59	A Method Based on MSVL for Verification of the Social Network Privacy Policy	会议论文	Xiaobing Wang\|Xiaobing Wang\|Tao Sun\|Tao Sun\|
60	Model checking Petri nets with MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Mengchu Zhou\|Mengchu Zhou\|
61	Time Constraints with Temporal Logic Programming	会议论文	Meng Han\|Zhenhua Duan\|Xiaobing Wang\|
62	symbolic model checking for embedded systems: a case study	会议论文	Tao Pang\|Zhenhua Duan\|
63	陕西省科学技术一等奖	奖励	赵亮\|赵亮\|黄伯虎\|张琛\|
64	可信软件设计开发与验证的基础理论与关键技术	奖励	赵亮\|赵亮\|黄伯虎\|张琛\|
65	Verification of distributed systems with the axiomatic system of MSVL	期刊论文	Qian Ma\|Zhenhua Duan\|Nan Zhang\|Xiaobing Wang\|
66	Research on An Infectious Disease Transmission by Flocking Birds	期刊论文	Mingsheng Tang\|Xinjun Mao\|Zahia Guessoum\|
67	Normal form expressions of propositional projection temporal logic	会议论文	Zhenhua Duan\|Cong Tian\|Nan Zhang\|
68	A Decision Procedure for a Fragment of Linear Time Mu-Calculus	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
69	Model checking concurrent systems with MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
70	NuTL2PFG:νTL公式的可满足性检查	期刊论文	段振华\|段振华\|田聪\|田聪\|
71	Persistent and Nonviolent Steps and the Design of GALS Systems	期刊论文	Lukasz Mikulski\|Marta Pietkiewicz-Koutny\|Danil Sokolov\|Alex Yakovlev\|
72	Improved even order magic square construction algorithms and their applications in multi-user shared electronic accounts	期刊论文	Jie Li\|Jie Li\|Cong Tian\|Cong Tian\|
73	Rumor diffusion in an Interests-based dynamic social network	期刊论文	Mingsheng Tang\|Xinjun Mao\|Zahia Guessoum\|Huiping Zhou\|
74	Interval Temporal Logic Semantics of Box Algebra	会议论文	Hanna Klaudel\|Maciej Koutny\|Zhenhua Duan\|
75	Bounded Model Checking for Propositional Projection Temporal Logic	会议论文	Zhenhua Duan\|Cong Tian\|Mengfei Yang\|Jia He\|
76	Extending MSVL with Semaphore	会议论文	Xinfeng Shu\|Xinfeng Shu\|Zhenhua Duan\|Zhenhua Duan\|
77	OrgMAP: An Organization-based Approach for Multi-Agent Programming	会议论文	Xinjun Mao\|Yin Chen\|Yuekun Sun\|Huip\|
78	Verifying safety critical task scheduling systems in PPTL axiom system	期刊论文	Mengfei Yang\|Bin Gu\|Zhenhua Duan\|Cong Tian\|
79	Model checking rate-monotonic scheduler with TMSVL	会议论文	Jin Cui\|Zhenhua Duan\|Cong Tian\|
80	Extending MSVL with function calls	会议论文	Nan Zhang\|Zhenhua Duan\|Cong Tian\|
81	工作流网合成规则及其在流程设计中的应用	期刊论文	张曼\|段振华\|
82	An Extended Strange Planet Protocol	会议论文	Jin Liu\|Zhenhua Duan\|Cong Tian\|
83	Improved Even Order Magic Square Construction Algorithms and Their Applications	会议论文	Zhenhua Duan\|Jin Liu\|Jie Li\|Cong Tian\|
84	Symbolic Model Checking for Alternating Projection Temporal Logic	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
85	PPTL_Spin: A SPIN Based Model Checker for Propositional Projection Temporal Logic	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
86	面向Agent程序设计研究综述	期刊论文	毛新军\|胡翠云\|王怀民\|
87	A canonical form based decision procedure and model checking approach for propositional projection temporal logic	期刊论文	Zhenhua Duan\|Cong Tian\|Nan Zhang\|
88	性能非对称多核处理器上的自适应调度	期刊论文	聂鹏程\|段振华\|田聪\|杨孟飞\|
89	Verification of A Real Time Scheduling Protocol of Safety-Critical Systems	会议论文	Cong Tian\|Cong Tian\|Nan Zhang\|Nan Zhang\|
90	A mechanism of function calls in MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
91	A Formal Engineering Framework for Service-based Software Modeling	期刊论文	Weikai Miao\|Shaoying Liu\|
92	Simulations of Influenza Viruses Transmission in Multiple Social Networks with an Artificial Society Model	期刊论文	Mingsheng Tang\|Xinjun Mao\|Huiping Zhou\|
93	A Decision Procedure for a Fragment of Linear Time Mu-Calculus	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
94	二维逻辑PPTLSL的可满足性检查	期刊论文	段振华\|段振华\|田聪\|田聪\|
95	Modeling and Verification of RBC Handover Protocol	期刊论文	Kai Yang\|Zhenhua Duan\|Cong Tian\|
96	Developing Self-Organizing Systems by Policy-based Self-Organizing Multi-Agent Systems	会议论文	Xinjun Mao\|Cuiyun Hu\|Junwen Yin\|Xinzhong Zhu\|
97	Detecting Spurious Counterexamples Efficiently in Abstract Model Checking	会议论文	Cong Tian\|Zhenhua Duan\|
98	Making CEGAR More Efficient in Software Model Checking	期刊论文	Cong Tian\|Zhenhua Duan\|
99	Abstract Model Checking with SOFL Hierachy	会议论文	Cong Tian\|Shaoying Liu\|Zhenhua Duan\|
100	ASML: Artificial Society Modelling Language for ACP Approach Based on Organization Metaphors	会议论文	Mingsheng Tang\|XinJun Mao\|Huiping Zhou\|Xueyan\|
101	An Approach to City-scale Artificial Society Modelling Based-on Organization Metaphor	会议论文	Mingsheng Tang\|Xinjun Mao\|Huiping Zhou\|Xueyan\|
102	Improved Net Reductions for LTLX Model Checking	会议论文	Ya Shi\|Zhenhua Duan\|Cong Tian\|Hua Yang\|
103	Data Resources in Dynamic Environments	会议论文	Wen Zeng\|Maciej Koutny\|
104	Present-Future Form of Linear Time $$\mu $$ -Calculus	会议论文	Yao Liu\|Zhenhua Duan\|Cong Tian\|Bo Liu\|
105	Translation from Workflow Nets to MSVL	会议论文	Ya Shi\|Zhenhua Duan\|Cong Tian\|
106	An MSVL Proof System in Coq	会议论文	Nan Zhang\|Nan Zhang\|Cong Tian\|Cong Tian\|
107	Localities in systems with a/sync communication	期刊论文	Jetty Kleijn\|Maciej Koutny\|
108	Making Automatic Repair for Large-scale Programs More Efficient Using Weak Recompilation	会议论文	Yuhua Qi\|Xiaoguang Mao\|Yan Lei\|
109	Test case generation from conjunctions of predicates with model checking	期刊论文	Cong Tian\|Shaoying Liu\|Zhenhua Duan\|
110	Satisfiability of Linear Time Mu-Calculus on Finite Traces	会议论文	Cong Tian\|Cong Tian\|Bin Cui\|Bin Cui\|
111	陕西省科学技术一等奖	奖励	赵亮\|赵亮\|黄伯虎\|张琛\|
112	Deternimization of Büchi Automata as Partitioned Automata	会议论文	Cong Tian\|Zhenhua Duan\|Mengfei Yang\|
113	A complete proof system for propositional projection temporal logic	期刊论文	Zhenhua Duan\|Nan Zhang\|Maciej Koutny\|
114	A formal proof of the deadline driven scheduler in PPTL axiomatic system	期刊论文	Nan Zhang\|Zhenhua Duan\|Cong Tian\|Dingzhu Du\|
115	Model Checking μC/OS-III Multi-task System with TMSVL	会议论文	Nan Zhang\|Nan Zhang\|Conghao Zhou\|Conghao Zhou\|
116	Transformation from business process models to BPEL with overlapped patterns involved	期刊论文	Man Zhang\|Zhenhua Duan\|
117	Performance Modelling and Evaluation of Enterprise Information Security technologies	会议论文	Wen Zeng\|Maciej Koutny\|Aad P. A. van Moorsel\|
118	Verilog程序的命题投影时序逻辑符号模型检测	期刊论文	逄涛\|段振华\|刘晓芳\|
119	教育部高等学校科学研究优秀成果自然科学一等	奖励	堵宏伟\|堵宏伟\|张南\|张南\|
120	Oragentburg: A Platform Supporting Organisation-based Programming	会议论文	Yan Chen\|Xinjun Mao\|Cuiyun Hu\|
121	Verify Heaps via Unified Model Checking	期刊论文	Xu Lu\|Zhenhua Duan\|Cong Tian\|Hongwei Du\|
122	PPTL_Spin: A SPIN Based Model Checker for Propositional Projection Temporal Logic	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
123	程序验证的基础理论研究	奖励	堵宏伟\|堵宏伟\|张南\|张南\|
124	Transformation from PLTL to Automata via NFGs	期刊论文	Cong Tian\|Zhenhua Duan\|
125	Secure communications with strange planet protocol	期刊论文	Cong Tian\|Zhenhua Duan\|Jin Liu\|
126	Regions of Petri nets with a/sync connections	期刊论文	Jetty Kleijn\|Maciej Koutny\|
127	Some Fixed-Point Issues in PPTL	会议论文	Zhenhua Duan\|Qian Ma\|Cong Tian\|Nan Zhang\|
128	Model Checking MSVL Programs Based on Dynamic Symbolic Execution	会议论文	Tian, Cong\|Cong Tian\|Zhang, Nan\|Nan Zhang\|
129	MSVL: A Typed Language for Temporal Logic Programming	期刊论文	Xiaobing Wang\|Cong Tian\|Zhenhua Duan\|Liang Zhao\|
130	WISHBONE片上总线符号模型检测	期刊论文	逄涛\|段振华\|
131	A complete axiom system for propositional projection temporal logic with cylinder computation model	期刊论文	Nan Zhang\|Zhenhua Duan\|Cong Tian\|
132	A Formal Proof of Deadline Driven Algorithms in Propositional Projection Temporal Logic	期刊论文	Nan Zhang\|Zhenhua Duan\|Cong Tian\|Dingzhu Du\|
133	Verification of A Real Time Scheduling Protocol of Safety-Critical Systems	会议论文	Cong Tian\|Cong Tian\|Nan Zhang\|Nan Zhang\|
134	Step Persistence in the Design of GALS Systems	会议论文	Maciej Koutny\|Marta Pietkiewicz-Koutny\|Danil Sokolov\|Alex Yakovlev\|
135	Model checking of pushdown systems for projection temporal logic	期刊论文	Liang Zhao\|Xiaobing Wang\|Zhenhua Duan\|
136	Improved even order magic square construction algorithms and their applications in multi-user shared electronic accounts	期刊论文	Jie Li\|Jie Li\|Cong Tian\|Cong Tian\|
137	Using Unified Model Checking to Verify Heaps	会议论文	Zhenhua Duan\|Zhenhua Duan\|Cong Tian\|Cong Tian\|
138	Efficient and scalable scheduling for performance heterogeneous multicore systems	期刊论文	Pengcheng Nie\|Zhenhua Duan\|
139	Unified Bounded Model Checking for MSVL	会议论文	Bin Yu\|Zhenhua Duan\|Cong Tian\|
140	An MSVL Proof System in Coq	会议论文	Nan Zhang\|Nan Zhang\|Cong Tian\|Cong Tian\|
141	Model checking Petri nets with MSVL	期刊论文	Zhenhua Duan\|Zhenhua Duan\|Mengchu Zhou\|Mengchu Zhou\|

查看更多信息请先登录或注册

再问科研

相关项目

趋势报告

经验分享