位置：成果数据库 > 会议 > 会议详情页
Formal Analysis of AODV Using Rely-Guarantee
  • 所属机构名称：华东师范大学
  • 会议名称：Proc. TASE 2013: 7th IEEE International Symposium on Theoretical Aspects of Software Engineering
  • 时间：2013.7.7
  • 成果类型：会议
  • 相关项目：信息物理融合系统的基础研究
作者： Wu Xiaofeng|Xu Qiwen|Zhu Huibiao|
同会议论文项目
信息物理融合系统的基础研究
期刊论文 10 会议论文 55 获奖 1 专利 1
同项目会议论文
Formal Approaches to Wireless Sensor Networks
Formalising the Continuous/Discrete Modeling
Formal Approaches to Mode Conversion and Positioning for Vehicle System
From Requirements to Development: Methodology and Example
Linking the Semantics of BPEL using Maude
Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts
Modelling and Analysis of Smart Grid: A Stochastic Model Checking Case Study
Linking Operational Semantics and Algebraic Semantics for Wireless Networks
ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System
A Calculus for Mobile Ad Hoc Networks from a Probabilistic Perspective
Formalizing Hybrid Systems with Event-B
Denotational Semantics for a Probability Timed Shared-Variable Language
The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs
A Denotational Model for Interrupt-Driven Programs
A Timing Verification Framework for AUTOSAR OS Component Development based on Real-Time Maude
Combinatorial Testing on ID3v2 Tags of MP3 Files
A Unifying Approach to Validating Specification-Oriented XML Constraints
Towards a Probabilistic Calculus for Mobile Ad Hoc Networks
Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions
Formal Modelling and Analysis of AODV
A Type System for SPARDL
Lattice-Valued Kripke Structures Based on Complete Residuated Lattice
Bisimulation for Lattice-valued Transition Systems
Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic
Formal Model of Interrupt Program from a Probabilistic Perspective
Modeling and Verifying the Code-Level OSEK/VDX Operating System With CSP
Approximate Simulation for Metric Hybrid Input/Output Automata
Formalizing Application Programming Interfaces of the OSEK Operating System
An Event-B Interpretation for SPARDL Model
Continuous Behaviour in Event-B: A Sketch
A Clock-based Framework for Construction of Hybrid Systems
Hybrid Relation Calculus
Towards a Modeling Language for Cyber-Physical Systems
Modeling and Verifying the Ariadne Protocol Using CSP
ASM and Controller Synthesis
Investigating Time Properties of Interrupt-Driven ProgramsProc SBMF 2012: 15th Brazilian Symposium o
Complementary Methodologies for Developing Hybrid Systems with Event-B
Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog using Maude
A Denotational Model for Instantaneous Signal Calculus
xBIL–A Hardware Resource Oriented Binary Intermediate Language
Formal Verification and Simulation: Co-Verification for Subway Control Systems
LTL Satisfiability Checking Revisited
Requirement Specification for Transportation Cyber Physical Systems
Multi-View Approach for Modeling Aerospace Cyber-Physical System
Towards a Signal Calculus for Event-Based Syn-chronous Languages
Formal Specification of Automatic DMARF based on CSP
Modeling and Analyzing the \muTESLA Protocol using CSP
Continuous ASM, and a Pacemaker Sensing Fragment
Modeling and Verification of AUTOSAR OS and EMS Application
A Timed CSP Model for the Time-Triggered Language Giotto
Cascade: A Test Generation Tool for Combinatorial Testing
Profile Directed Systematic Testing of Concurrent Programs
MDM: A Mode Diagram Modeling Framework
An Approach to Requirement Analysis for Periodic Control Systems