[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Wang et al., 2015 - Google Patents

An improved HHL prover: an interactive theorem prover for hybrid systems

Wang et al., 2015

View PDF
Document ID
3874757898298316335
Author
Wang S
Zhan N
Zou L
Publication year
Publication venue
Formal Methods and Software Engineering: 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings 17

External Links

Snippet

Hybrid systems are integrations of discrete computation and continuous physical evolution. To guarantee the correctness of hybrid systems, formal techniques on modelling and verification of hybrid systems have been proposed. Hybrid CSP (HCSP) is an extension of …
Continue reading at drive.google.com (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/5022—Logic simulation, e.g. for logic circuit operation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5045—Circuit design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • G06F8/34—Graphical or visual programming
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/04—Inference methods or devices
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N99/00—Subject matter not provided for in other groups of this subclass
    • G06N99/005—Learning machines, i.e. computer in which a programme is changed according to experience gained by the machine itself during a complete run
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/10—Requirements analysis; Specification techniques
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/86—Hardware-Software co-design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing

Similar Documents

Publication Publication Date Title
Wang et al. An improved HHL prover: an interactive theorem prover for hybrid systems
Fitzgerald et al. Collaborative design for embedded systems
Chen et al. MARS: A toolchain for modelling, analysis and verification of hybrid systems
Cavalcanti et al. From control law diagrams to Ada via Circus
KR20150123282A (en) Method for securing a program
Foster et al. Towards a UTP semantics for Modelica
Wang et al. From design to implementation: an automated, credible autocoding chain for control systems
Hayes et al. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
Kamburjan et al. A hybrid programming language for formal modeling and verification of hybrid systems
Boulanger et al. Semantic adaptation using CCSL clock constraints
Foster et al. Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL: (Invited Tutorial)
Chen et al. A two-way path between formal and informal design of embedded systems
Ye et al. Compositional assume-guarantee reasoning of control law diagrams using UTP
Huerta y Munive Algebraic verification of hybrid systems in Isabelle/HOL
Yan et al. Approximate bisimulation and discretization of hybrid CSP
Silva et al. Test case generation from natural language requirements using cpn simulation
Durán et al. Statistical model checking of e-Motions domain-specific modeling languages
Foster et al. Towards verification of cyber-physical systems with UTP and Isabelle/HOL
Jesus et al. Compositional verification of Simulink block diagrams using tock-CSP and CSP-prover
Zhang et al. Proving Simulink block diagrams correct via refinement
Woodcock et al. Heterogeneous semantics and unifying theories
Wang Credible autocoding of control software.
Dupont Correct-by-construction design of hybrid systems based on refinement and proof
Guttmann et al. A Repository for Tarski-Kleene Algebras.
Tripakis Compositional model-based system design and other foundations for mastering change