Sökning: "formell specifikation"
Visar resultat 1 - 5 av 12 uppsatser innehållade orden formell specifikation.
1. Practical Analysis of the Giskard Consensus Protoco
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : Consensus protocols are the core of modern blockchain systems, such as the Bitcoin, Ethereum, and Algorand networks. Thanks to these protocols, participants in a blockchain network can reach consensus on which blocks to add to a blockchain, to have a consistent chain of blocks in the whole network. LÄS MER
2. Automated Inference of ACSL Contracts for Programs with Heaps
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. LÄS MER
3. A Specification for Time-Predictable Communication on TDM-based MPSoC Platforms
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : Formal System Design (ForSyDe) aims to bring the design of multiprocessor systems-on-chip (MPSoCs) to a higher level of abstraction and bridge the abstraction gap by transformational design refinement. The current research is focused on a correct-by-construction design flow, which requires design space exploration including formal models of computation and timepredictable platforms. LÄS MER
4. A Method for Porting Software Using Formal Specifications
Kandidat-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : Formal specifications are mathematically based techniques with which a system can be analyzed, and its functionalities be described. Case studies have shown that using formal specifications can help reduce bugs and other inconsistencies when implementing a complex system; they are more likely found during the software design phase rather than later. LÄS MER
5. Automated Annotation of Simulink Generated C Code Based on the Simulink Model
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : There has been a wave of transformation in the automotive industry in recent years, with most vehicular functions being controlled electron- ically instead of mechanically. This has led to an exponential increase in the complexity of software functions in vehicles, making it essential for manufactures to guarantee their correctness. LÄS MER