Font Size: a A A

Research On Formal Modeling,Verification And Scheduling Of Real-time Embedded Software

Posted on:2021-07-20Degree:DoctorType:Dissertation
Country:ChinaCandidate:Y J WangFull Text:PDF
GTID:1488306314999489Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
Currently,the application of embedded software is increasingly widespread,and the software scale is becoming larger and larger,often with tens of millions of lines of C source code,widely-used timers and complex logical structures.The characteristics of multiple levels of nesting of interrupts and the heterogeneity system including CPU,GPU and FPGA lead to extremely difficult software development and testing,and software trustworthiness is a major problem in security-critical industries.From the perspective of trusted software,embedded software trust should include functional trust and performance trust at least.The so-called functional trust refers to the software to complete the expected functions,namely the correctness of software execution.In addition,the performance trust refers to the software to complete the expected tasks within the prescribed time limit,without performance trust,it is meaningless even if the execution is correct.At present,the research on trusted software is more focused on functional trust,of which,some results have been achieved in software testing,software formal modeling,model simulation and verification,etc.However,the design for embedded system does not only need to solve the problem of functional trust,but also needs to solve the problem of performance trust.Performance trust mainly includes:(1)How to verify the correctness and time performance of the software?(2)How to analyze and schedule the interrupt-driven programs?(3)How to determine the task processing sequence to ensure the real-time performance of a multi-core embedded system?(4)How to reduce the energy consumption of an embedded system?Aiming at these above problems,the research focuses on the performance trust of the embedded system,and explores and studies from four aspects,including trust verification,interrupt scheduling,task scheduling and energy consumption optimization.The contents are organized as follows:?.Theoretical methods of embedded software requirement modeling and verificationA formal modeling method for embedded system requirements based on ESTM(Extended State Transition Matrix)is proposed to address the trust verification of embedded system requirements.STM adds a clock mapping function structure,which can effectively represent the transaction processing time so that ESTM model can display time attributes;for functional requirements verification,a TPTL(Timed Propositional Temporal Logic)model detection method based on BMC(Bounded Model Checking)technology is adopted,to detect whether there are missing requirements and logical contradictions in system requirements,to verify the system's functional attributes to ensure the correctness of software execution;for performance requirements verification,an MVMI(Model Verification Method based on Interpolation)is designed,which calculates the symbolic range of the program execution path complexity according to the event processing function and the state migration process,and the warning of potential problems for system performance.?.Formal modeling and scheduling of interrupt-driven programsIn real-time embedded software design,time predictability is a crucial factor to ensure software reliability.Therefore,time analysis is a very important and challenging issue.The research proposes a formal modeling method for interrupt-driven programs and an interrupt thread scheduling algorithm from the perspective of timing.Firstly,a formal method based on IESTM(Interrupt Extended State Transition Matrix)is proposed to model the interrupt-driven programs,the definition of operational semantics and program semantics is given,the time characteristics of the program are analyzed by using the semantics,and the security mechanism is provided to ensure the execution of the main program before the deadline.Secondly,the IEDF scheduling algorithm is proposed for interrupt thread scheduling,which could shorten the waiting time for interrupt thread execution and effectively reduce the deadline miss rate and the total time consumption of interrupt processing,to ensure the real-time performance of the system.?.Optimal scheduling model for multi-core embedded real-time systemsIn embedded real-time systems,the real-time performance of tasks is not only to ensure the timely response of tasks,but also more importantly to ensure timely completion of tasks.That is,while ensuring real-time performance of high-priority tasks,it is also necessary to ensure real-time performance of low priority tasks as far as possible so as to ensure the real-time performance of the whole system.This research proposes an optimal scheduling model for multi-core embedded real-time systems.This model adopts a decentralized scheduling method to configure a two-level scheduling algorithm.The major function of the first-level scheduling algorithm is to allocate tasks for multiple cores,with the main purpose of reducing the total waiting time of tasks on each core.The major function of the second-level scheduling algorithm is to schedule tasks on each core,and the main purpose is to ensure the real-time performance of the whole system,then a scheduling algorithm for inserting a delay time is designed.?.Dynamic adjustment model of energy consumption perception in an embedded real-time systemEmbedded systems generally work in energy-constrained environment.Therefore,energyconsuming factors must be considered on the premise of satisfying CPU computing performance.The research proposes an energy-aware adjustment model for embedded real-time systems,which combines task scheduling and energy consumption management to ensure that tasks can be completed before the deadline and minimize processor energy consumption as much as possible.Based on the consideration of timing sequence control and energy consumption control,a dynamic energy consumption management scheduling algorithm is designed to fully explore the task deadline and system energy consumption adjustment under the condition of multiple preemption tasks.DVFS technology is adopted to reduce system energy consumption while meeting the deadline.
Keywords/Search Tags:Software Trusted Verification, Bounded Model Checking, Scheduling Strat-egy, Energy Consumption Optimization
PDF Full Text Request
Related items