位置：成果数据库 > 会议 > 会议详情页
From Requirements to Development: Methodology and Example
  • 所属机构名称：华东师范大学
  • 会议名称：Proc. ICFEM 2011: 13th International Conference on Formal Engineering Methods, Spinger-Verlag, LNCS
  • 时间：2011.10.10
  • 成果类型：会议
  • 相关项目：信息物理融合系统的基础研究
作者： Su Wen|Jean-Raymond Abrial|Huang Runlei|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
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
Formal Analysis of AODV Using Rely-Guarantee
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