Runtime analysis of synchronous programs for low-level real-time verification

被引：0
|
作者：
Logothetis, G [1 ]
Schneider, K [1 ]
Metzler, C [1 ]
机构：
[1] Univ Karlsruhe, Inst Comp Design & Fault Tolerance, D-76128 Karlsruhe, Germany
来源：
16TH SYMPOSIUM ON INTEGRATED CIRCUITS AND SYSTEMS DESIGN, SBCCI 2003, PROCEEDINGS | 2003年
关键词：
D O I：
10.1109/SBCCI.2003.1232831
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Synchronous programming languages are well-suited for the implementation and verification of real-time systems. The main benefit for the estimation of real-time constraints is thereby that the macro steps provided by the semantics of synchronous languages can be directly used as building blocks for runtime analysis. We describe a new approach to determine the execution times of the macro steps of a synchronous program wrt. given microprocessors and generate real-time formal models endowed with notions of physical time for formal verification purposes. The execution times are exact, since we consider all possible input sequences.
引用
收藏
页码：211 / 216
页数：6
相关论文
共 50 条
  • [41] Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic
    Chlipala, Adam
    ACM SIGPLAN NOTICES, 2011, 46 (06) : 234 - 245
  • [42] Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic
    Chlipala, Adam
    PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2011, : 234 - 245
  • [43] Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs
    Tsai, Ming-Hsien
    Wang, Bow-Yaw
    Yang, Bo-Yin
    CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, 2017, : 1973 - 1987
  • [44] Runtime verification of real-time event streams under non-synchronized arrival
    Martin Leucker
    César Sánchez
    Torben Scheffel
    Malte Schmitz
    Alexander Schramm
    Software Quality Journal, 2020, 28 : 745 - 787
  • [45] Runtime verification of real-time event streams under non-synchronized arrival
    Leucker, Martin
    Sanchez, Cesar
    Scheffel, Torben
    Schmitz, Malte
    Schramm, Alexander
    SOFTWARE QUALITY JOURNAL, 2020, 28 (02) : 745 - 787
  • [46] Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I
    Aurandt, Alexis
    Jones, Phillip H.
    Rozier, Kristin Yvonne
    NASA FORMAL METHODS (NFM 2022), 2022, 13260 : 816 - 825
  • [47] THE REAL-TIME VERIFICATION
    PELTOLA, S
    MEDICAL PHYSICS, 1988, 15 (05) : 799 - 799
  • [48] HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
    Gorostiaga, Felipe
    Sanchez, Cesar
    FORMAL METHODS, FM 2021, 2021, 13047 : 563 - 580
  • [49] A framework for static analysis and verification of low-level RTOS code
    Manjunath, Vignesh
    Baunach, Marcel
    JOURNAL OF SYSTEMS ARCHITECTURE, 2024, 154
  • [50] GPU-based Low-Level Trigger System for Real-Time Cherenkov Ring Fitting
    Ammendola, R.
    Biagioni, A.
    Chiozzi, S.
    Ramusino, A. Cotta
    Fantechi, R.
    Fiorini, M.
    Frezza, O.
    Gianoli, A.
    Lamanna, G.
    Lo Cicero, F.
    Lonardo, A.
    Martinelli, M.
    Neri, I.
    Paolucci, P. S.
    Pastorelli, E.
    Piandani, R.
    Piccini, M.
    Pontisso, L.
    Rossetti, D.
    Santoni, C.
    Simula, F.
    Sozzi, M.
    Tosoratto, L.
    Vicini, P.
    2015 IEEE NUCLEAR SCIENCE SYMPOSIUM AND MEDICAL IMAGING CONFERENCE (NSS/MIC), 2015,
12345