形式方法和软件工程LNCS-4260

形式方法和软件工程LNCS-4260
作 者: Zhiming Liu
出版社: 湖南文艺出版社
丛编项:
版权说明: 本书为公共版权或经版权方授权,请支持正版图书
标 签: 暂缺
ISBN 出版时间 包装 开本 页数 字数
未知 暂无 暂无 未知 0 暂无

作者简介

暂缺《形式方法和软件工程LNCS-4260》作者简介

内容简介

This book constitutes the refereed proceedings of the 8th International Conference on Formal Engineering Methods, ICFEM 2006, held in Macao, China, in November 2006.The 38 revised full papers presented together with 3 keynote talks were carefully reviewed and selected from 108 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on specification and verification, internetware and Web-based systems, concurrent, communicating, timing and probabilistic systems, object and component orientation, testing and model checking, tools, fault-tolerance and security, as well as specification and refinement.

图书目录

Keynote Talks

 Program Verification Through Computer Algebra

 JML's Rich, Inherited Specifications for Behavioral Subtypes

 Three Perspectives in Formal Engineering

Specification and Verification

 A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces

 Applying Timed Interval Calculus to Simulink Diagrams

 Reducing Model Checking of the Few to the One

 Induction-Guided Falsification

 Verifying x Models of Industrial Systems with SPIN

 Stateful Dynamic Partial-Order Reduction

Internetware and Web-Based Systems

 User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition 

 Environment Ontology-Based Capability Specification for Web Service Discovery

 Scenario-Based Component Behavior Derivation

 Verification of Computation Orchestration Via Timed Automata

 Towards the Semantics for Web Service Choreography Description Language

 Type Checking Choreography Description Language

Concurrent, Communicating, Timing and Probabilistic Systems

 Formalising Progress Properties of Non-blocking Programs

 Towards a Fully Generic Theory of Data

 Verifying Statemate Statecharts Using CSP and FDR

 A Reasoning Method for Timed CSP Based on Constraint Solving

 Mapping RT-LOTOS Specifications into Time Petri Nets

 Reasoning Algebraically About Probabilistic Loops

Object and Component Orientation

Testing and Model Checking

Tools

Fault-Tolerance and Security

Specification and Refinement

Author Index