Sökning: "Bounded Model Checking"

Hittade 3 uppsatser innehållade orden Bounded Model Checking.

1. 1. Implementation and evaluation of bounded invariant model checking for a subset of Stateflow

   Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Gustav Ung; [2021]
   Nyckelord :Formal methods; Bounded Model Checking; Stateflow; SLDV; Formella metoder; Begränsad modellprovning; Stateflow; SLDV;

   Sammanfattning : Stateflowmodels are used for describing logic and implementing state machines in modern safety-critical software. However, the complete Stateflowmodelling language is hard to formally define, therefore a subset relevant for industrial models has been developed in previous works. LÄS MER

3. 2. Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs

   Master-uppsats, Uppsala universitet/Institutionen för informationsteknologi

   Författare :Shahrzad Khodayari; [2014]
   Nyckelord :;

   Sammanfattning : Embedded systems are widely used in most electrical devices. They are often complex and safety-critical. Therefore, their reilability is significantlyimportant. AMong many techniques to verify a system, model checking models a system into temporal logic and can be used to assert a desired property on it. LÄS MER

4. 3. Model checking of multicore software using CBMC

   Master-uppsats, Institutionen för informationsteknologi

   Författare :Ashok Kelur; [2012]
   Nyckelord :;

   Sammanfattning : Computers have been key subsystems in various complex systems. As computers are adapted into various fields, hardware and software are increasing in size and complexity. It is evident that parallel computing is the way to solve large scale complex information technology problems. LÄS MER