1. TASE 2007: Shanghai, China

Tutorial

• Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Laurent Mauborgne, David Monniaux, Xavier Rival:
  Varieties of Static Analyzers: A Comparison with ASTREE. 3-20
  

Keynote Speech Abstracts

• Jeannette M. Wing:
  Software Security. 21
  
• Mathai Joseph:
  Abstractions for Real Real-time Systems. 22
  

Verification and Validation 1

• Edd Turner, Michael Leuschel, Corinna Spermann, Michael J. Butler:
  Symmetry Reduced Model Checking for B. 25-34
  
• Jinzhao Wu, Lin Zhao:
  Multi-Valued Model Checking via Groebner Basis Approach. 35-44
  
• Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg, Felix Rauch:
  Model Checking Software at Compile Time. 45-56
  
• Zhiming Chang, XinJun Mao, Zhichang Qi:
  An Approach based on Bigraphical Reactive Systems to Check Architectural Instance Conforming to its Style. 57-66
  
• Paolo Zuliani:
  A Formal Derivation of Grover's Quantum Search Algorithm. 67-74
  
• Fei Xu, Li Zhang:
  Unified Modeling and Analysis based on Petri nets and Pi calculus. 75-86
  

Software Architecture and Frameworks 1

• Cong-Cong Xing:
  An Object Type Graph System. 87-96
  
• Jiancheng Ni, Zhishu Li, Jirong Sun, Jianchuan Xing:
  Self-adaptive Intrusion Detection System for Computational Grid. 97-106
  

Security Issues

• Maria João Frade, Ando Saabas, Tarmo Uustalu:
  Foundational certification of data-flow analyses. 107-116
  
• Yu Guo, Xinyu Jiang, Yiyun Chen, Chunxiao Lin:
  A Certified Thread Library for Multithreaded User Programs. 117-126
  
• Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu:
  Design of a Certifying Compiler Supporting Proof of Program Safety. 127-138
  

Testing Techniques

• X. W. Huang, L. Jiao, W. M. Lu:
  A Semantic Preorder on Refinement and Fairness. 139-148
  
• Mercedes G. Merayo, Manuel Núñez, Ismael Rodríguez:
  Generation of optimal finite test suites for timed systems. 149-158
  
• Marc Aiguier, Delphine Longuet:
  Test Selection Criteria for Modal Specifications of Reactive Systems. 159-170
  

Workflow Analysis

• Jiacun Wang, William M. Tepfenhart, Daniela Rosca, Anni Tsai:
  Resource-Constrained Workflow Modeling. 171-177
  
• Yunni Xia, Hanpin Wang, Yu Huang, Wanling Qu:
  Queuing analysis and performance evaluation of workflow through WFQN. 178-187
  
• Fei Xu, Zhiwei Yu:
  A Workflow Verification Method Based on Calculus. 188-196
  
• Alexander Förster, Gregor Engels, Tim Schattkowsky, Ragnhild Van Der Straeten:
  Verification of Business Process Quality Constraints Based on Visual Process Patterns. 197-208
  

Verification and Validation 2

• Fei Pu, Wenhui Zhang:
  Partition Refinement in Abstract Model Checking. 209-218
  
• Cyrille Artho, Christian Sommer, Shinichi Honiden:
  Model Checking Networked Programs in the Presence of Transmission Failures. 219-228
  
• Naiyong Jin, Chengjie Shen:
  Dynamic Verifying The Properties of The Simple Subset of PSL. 229-240
  

Formal Methods 2

• Donghuo Chen, Guangquan Zhang, Jinzhao Wu:
  QCTL: A Logic for Reasoning about Inconsistent Concurrent Systems. 241-250
  
• Yongtao Ma, Zhenhua Duan, Xiaobing Wang, Xiaoxiao Yang:
  An Interpreter for Framed Tempura and Its Application. 251-260
  
• Lingzhong Zhao, Tianlong Gu, Junyan Qian:
  Goal-independent Semantics for Path Dependent Analysis of Prolog Programs. 261-272
  

Software Architecture and Frameworks 2

• Howard Barringer, David E. Rydeheard, Dov M. Gabbay:
  A Logical Framework for Monitoring and Evolving Software Components. 273-282
  
• Jing Dong, Tu Peng, Zongyan Qiu:
  Commutability of Design Pattern Instantiation and Integration. 283-292
  
• Hung Ledang, Dang Van Hung:
  Timing and Concurrency Specification in Component-based Real-Time Embedded Systems Development. 293-304
  

Safety and Reliability

• Markus Pizka, Elmar Jürgens:
  Automating Language Evolution. 305-315
  
• Franck Cassez, Stavros Tripakis, Karine Altisen:
  Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems. 316-325
  
• Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo:
  Foundational Typed Assembly Language with Certified Garbage Collection. 326-338
  

Verification and Validation 3

• Yanyan Xu, Wei Chen, Liang Xu, Wenhui Zhang:
  Evaluation of SAT-based Bounded Model Checking of ACTL Properties. 339-348
  
• Hongwei Zeng, Huaikou Miao, Jing Liu:
  Specification-based Test Generation and Optimization Using Model Checking. 349-355
  
• Viliam Holub, Petr Tuma:
  Streaming State Space: A Method of Distributed Model Verification. 356-368
  

Formal Methods 3

• Phan C. Vinh, Jonathan P. Bowen:
  A Formal Approach to Aspect-Oriented Modular Reconfigurable Computing. 369-378
  
• Hai H. Wang, Shengchao Qin, Jun Sun, Jin Song Dong:
  Realizing Live Sequence Charts in SystemVerilog. 379-388
  
• Sun Meng:
  QCCS: A Formal Model to Enforce QoS Requirements in Service Composition. 389-400
  

Software Architecture and Frameworks 3

• Yifeng Sun, David Levy:
  A Software Process for Modeling Complex Systems with UML-RT. 401-410
  
• Ingo Feinerer, Gernot Salzer:
  Consistency and Minimality of UML Class Specifications with Multiplicities and Uniqueness Constraints. 411-420
  
• Tun Lu, Ning Gu:
  Survivability-Aware Configuration Management of Service-Oriented System Based on Service Dependency. 421-432
  

Formal Methods 4

• Shengyuan Wang, Yuan Dong:
  Improving Combinability of Petri Nets with Inheritance, Aggregation and Association. 433-439
  
• Jeff W. Sanders, Matteo Turilli:
  Dynamics of Control. 440-449
  
• Jianmin Jiang, Jinzhao Wu, Hongping Shu:
  Symmetry in Process Algebra. 450-462
  

Service Systems

• Maria Grazia Buscemi, Laura Ferrari, Corrado Moiso, Ugo Montanari:
  Constraint-Based Policy Negotiation and Enforcement for Telco Services. 463-472
  
• Jing Li, Huibiao Zhu, Geguang Pu:
  Conformance Validation between Choreography and Orchestration. 473-482
  
• Wen-jun Li, Xiao-jun Liang, Hua-mei Song, Xiaocong Zhou:
  QoS-Driven Service Composition Modeling with Extended Hierarchical CPN. 483-492