The Community for Technology Leaders
2012 Sixth International Symposium on Theoretical Aspects of Software Engineering (2007)
Shanghai, China
June 6, 2007 to June 8, 2007
ISBN: 0-7695-2856-2
TABLE OF CONTENTS
Introduction

Reviewers (PDF)

pp. xii
Tutorial

Varieties of Static Analyzers: A Comparison with ASTREE (Abstract)

Jerome FERET , Ecole Normale Superieure, France
David MONNIAUX , CNRS, Ecole Normale Superieure, France
Radhia COUSOT , CNRS, Ecole Polytechnique, France
Laurent MAUBORGNE , Ecole Normale Superieure, France
Xavier RIVAL , Ecole Normale Superieure, France
Antoine MINE , Ecole Normale Superieure, France
Patrick COUSOT , Ecole Normale Superieure, France
pp. 3-20
Keynote Speech Abstracts

Software Security (PDF)

Jeannette M. Wing , Carnegie Mellon University
pp. 21

Abstractions for Real Real-time Systems (PDF)

Mathai Joseph , Tata Consultancy Services
pp. 22
Verification and Validation 1

Symmetry Reduced Model Checking for B (Abstract)

Edd Turner , University of Southampton
Corinna Spermann , Universitat Dusseldorf Universitatsstr, Germany
Michael Butler , University of Southampton
Michael Leuschel , Universitat Dusseldorf Universitatsstr, Germany
pp. 25-34

Multi-Valued Model Checking via Groebner Basis Approach (Abstract)

Jinzhao Wu , University of Electronic Science and Technology
Lin Zhao , Chinese Academy of Sciences
pp. 35-44

Model Checking Software at Compile Time (Abstract)

Patrick Jayet , University of New South Wales, Australia
Ralf Huuck , University of New South Wales, Australia
Michel Lussenburg , University of New South Wales, Australia
Felix Rauch , University of New South Wales, Australia
Ansgar Fehnker , University of New South Wales, Australia
pp. 45-56
Formal Methods 1

An Approach based on Bigraphical Reactive Systems to Check Architectural Instance Conforming to its Style (Abstract)

Xinjun Mao , National University of Defense Technology
Zhichang Qi , National University of Defense Technology
Zhiming Chang , National University of Defense Technology
pp. 57-66

Unified Modeling and Analysis based on Petri nets and Pi calculus (Abstract)

Li Zhang , Tsinghua University
Fei Xu , Tsinghua University
pp. 75-86
Software Architecture and Frameworks 1

An Object Type Graph System (Abstract)

Cong-Cong Xing , Nicholls State University
pp. 87-96

Self-adaptive Intrusion Detection System for Computational Grid (Abstract)

SUN Jirong , Sichuan University
LI Zhishu , Sichuan University
NI Jiancheng , Qufu Normal University, Rizhao 276826, CHINA
XING Jianchuan , Sichuan University
pp. 97-106
Security Issues

Foundational certification of data-flow analyses (Abstract)

Maria Joao Frade , Universidade do Minho
Tarmo Uustalu , Tallinn University of Technology
Ando Saabas , Tallinn University of Technology
pp. 107-116

A Certified Thread Library for Multithreaded User Programs (Abstract)

Yu Guo , University of Science and Technology of China
Xinyu Jiang , University of Science and Technology of China
Chunxiao Lin , University of Science and Technology of China
Yiyun Chen , University of Science and Technology of China
pp. 117-126

Design of a Certifying Compiler Supporting Proof of Program Safety (Abstract)

Cheng Liu , University of Science and Technology of China
Baojian Hua , University of Science and Technology of China
Lin Ge , University of Science and Technology of China
Yiyun Chen , University of Science and Technology of China
Zhaopeng Li , University of Science and Technology of China
pp. 127-138
Testing Techniques

A Semantic Preorder on Refinement and Fairness (Abstract)

W.M. Lu , Chinese Academy of Sciences
X.W. Huang , Chinese Academy of Sciences
L. Jiao , Chinese Academy of Sciences
pp. 139-148

Generation of optimal finite test suites for timed systems (Abstract)

Ismael Rodriguez , Universidad Complutense de Madrid, E-28040 Madrid. Spain.
Mercedes G. Merayo , Universidad Complutense de Madrid, E-28040 Madrid. Spain.
Manuel Nunez , Universidad Complutense de Madrid, E-28040 Madrid. Spain.
pp. 149-158

Test Selection Criteria for Modal Specifications of Reactive Systems (Abstract)

Marc Aiguier , University of Evry Val d?Essonne
Delphine Longuet , University of Evry Val d?Essonne
pp. 159-170
Workflow Analysis

Resource-Constrained Workflow Modeling (Abstract)

Daniela Rosca , Monmouth University
Jiacun Wang , Monmouth University
Anni Tsai , Monmouth University
William Tepfenhart , Monmouth University
pp. 171-177

Queuing analysis and performance evaluation of workflow through WFQN (Abstract)

Hanpin Wang , Peking University
Yu Huang , Peking University
Yunni Xia , Peking University
Wanling Qu , Peking University
pp. 178-187

A Workflow Verification Method Based on Calculus. (Abstract)

Fei Xu , Tsinghua University
Zhiwei Yu , Tsinghua University
pp. 188-196

Verification of Business Process Quality Constraints Based on Visual Process Patterns (Abstract)

Gregor Engels , University of Paderborn
Tim Schattkowsky , University of Paderborn
Alexander Forster , University of Paderborn
Ragnhild Van Der Straeten , Vrije Universiteit Brussel
pp. 197-208
Verification and Validation 2

Partition Refinement in Abstract Model Checking (Abstract)

Wenhui Zhang , Chinese Academy of Sciences
Fei Pu , Chinese Academy of Sciences
pp. 209-218

Model Checking Networked Programs in the Presence of Transmission Failures (Abstract)

Shinichi Honiden , National Institute of Informatics, Tokyo, Japan
Cyrille Artho , National Institute of Informatics, Tokyo, Japan
Christian Sommer , ETH Z?rich, Zurich, Switzerland
pp. 219-228

Dynamic Verifying The Properties of The Simple Subset of PSL (Abstract)

Chengjie Shen , East China Normal University
Naiyong Jin , East China Normal University
pp. 229-240
Formal Methods 2

QCTL: A Logic for Reasoning about Inconsistent Concurrent Systems (Abstract)

Guangquan Zhang , Soochow University
Jinzhao Wu , Soochow University
Donghuo Chen , Soochow University
pp. 241-250

An Interpreter for Framed Tempura and Its Application (Abstract)

Yongtao Ma , Xidian University,Xi?an, 710071, P.R. China
Xiaoxiao Yang , Xidian University,Xi?an, 710071, P.R. China
Xiaobing Wang , Xidian University,Xi?an, 710071, P.R. China
Zhenhua Duan , Xidian University,Xi?an, 710071, P.R. China
pp. 251-260

Goal-independent Semantics for Path Dependent Analysis of Prolog Programs (Abstract)

Junyan Qian , Guilin University Electronic Technology
Tianlong Gu , Guilin University Electronic Technology
Lingzhong Zhao , Guilin University Electronic Technology
pp. 261-272
Software Architecture and Frameworks 2

A Logical Framework for Monitoring and Evolving Software Components (Abstract)

David Rydeheard , University of Manchester
Dov Gabbay , Kings College London
Howard Barringer , University of Manchester
pp. 273-282

Commutability of Design Pattern Instantiation and Integration (Abstract)

Jing Dong , University of Texas at Dallas
Zongyan Qiu , Peking University
Tu Peng , University of Texas at Dallas
pp. 283-292
Safety and Reliability

Automating Language Evolution (Abstract)

Elmar Jurgens , Technische Universitat Munchen
Markus Pizka , Technische Universitat Munchen
pp. 305-315

Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems (Abstract)

Stavros Tripakis , Cadence Berkeley Labs, 1995 University Avenue, Berkeley, CA,
Franck Cassez , CNRS/IRCCyN, Cedex, France
Karine Altisen , INPG and Verimag Laboratory, France
pp. 316-325

Foundational Typed Assembly Language with Certified Garbage Collection (Abstract)

Yiyun Chen , University of Science and Technology of China
Chunxiao Lin , University of Science and Technology of China
Andrew McCreight , Yale University
Yu Guo , University of Science and Technology of China
Zhong Shao , Yale University
pp. 326-338
Verification and Validation 3

Evaluation of SAT-based Bounded Model Checking of ACTL Properties (Abstract)

Liang Xu , Chinese Academy of Sciences, Beijing, China
Wei Chen , Chinese Academy of Sciences, Beijing, China
Yanyan Xu , Chinese Academy of Sciences, Beijing, China
Wenhui Zhang , Chinese Academy of Sciences, Beijing, China
pp. 339-348

Specification-based Test Generation and Optimization Using Model Checking (Abstract)

Jing Liu , China Normal University, Shanghai 200062, China
Huaikou Miao , Shanghai University, Shanghai 200072, China
Hongwei Zeng , Wuhan University,
pp. 349-355

Streaming State Space: A Method of Distributed Model Verification (Abstract)

Petr Tuma , Charles University in Prague, Czech Republic
Viliam , Charles University in Prague, Czech Republic
pp. 356-368
Formal Methods 3

A Formal Approach to Aspect-Oriented Modular Reconfigurable Computing (Abstract)

Phan Cong-Vinh , London South Bank University
Jonathan P. Bowen , Museophile Limited, UK
pp. 369-378

Realizing Live Sequence Charts in SystemVerilog (Abstract)

Jin Song Dong , National University of Singapore
Hai H. Wang , University of Southampton
Jun Sun , National University of Singapore
Shengchao Qin , Durham University.
pp. 379-388

QCCS: A Formal Model to Enforce QoS Requirements in Service Composition (Abstract)

Sun Meng , CWI, Kruislaan 413, Amsterdam, The Netherlands
pp. 389-400
Software Architecture and Frameworks 3

A Software Process for Modeling Complex Systems with UML-RT (Abstract)

David Levy , University of Sydney, NSW 2006, Australia
Yifeng Sun , University of Sydney, NSW 2006, Australia
pp. 401-410
Formal Methods 4

Dynamics of Control (Abstract)

J W Sanders , United Nations University
Matteo Turilli , Oxford University Computing Laboratory
pp. 440-449

Symmetry in Process Algebra (Abstract)

Hongping Shu , Chengdu University of Information Technology
Jinzhao Wu , Chinese Academy of Sciences
Jianmin Jiang , Fujian Normal University
pp. 450-462
Service Systems

Constraint-Based Policy Negotiation and Enforcement for Telco Services (Abstract)

Ugo Montanari , University of Pisa, Italy
Laura Ferrari , Telecom Italia Lab, Italy
Corrado Moiso , Telecom Italia Lab, Italy
Maria Grazia Buscemi , IMT Lucca, Italy
pp. 463-472

Conformance Validation between Choreography and Orchestration (Abstract)

Geguang Pu , East China Normal University
Huibiao Zhu , East China Normal University
Jing Li , East China Normal University
pp. 473-482

QoS-Driven Service Composition Modeling with Extended Hierarchical CPN (Abstract)

Xiao-jun LIANG , Sun Yat-sen University
Wen-jun LI , Sun Yat-sen University
Xiao-cong ZHOU , Sun Yat-sen University
Hua-mei SONG , Sun Yat-sen University
pp. 483-492
Author Index

Author Index (PDF)

pp. 493
97 ms
(Ver )