1. Discrete time model for process meta language with fictitious-clockBoštjan Vlaovič, Aleksander Vreže, 2022, izvirni znanstveni članek Opis: Industries like telecommunications, medical, automotive, military, avionics, and aerospace
use complex real-time systems. Specification and Description Language (SDL) is one of the leading
domain specific languages that is formally defined by international standards and well established in
describing such systems. To check system properties abstracted model of the system is prepared in
selected modeling language. We use Spin (Simple Promela Interpreter) model checker that is one of
the leading tools for verification of complex concurrent and reactive systems. This paper focuses on
modeling the SDL timer construct. It is one of the SDL constructs that is not easily modeled with
Promela, but is present in many SDL systems. After an overview of the related work we propose
a new Discrete Time Model for Promela (DTMP) that is seamlessly integrated in our framework
for modeling SDL systems and can be used with the mainstream version of the Spin tool. To the
best of our knowledge, this is not possible with the existing solutions. We describe how DTMP can
be used to model SDL systems that use timers. Experimental results demonstrate its applicability
to non-SDL systems with Fischer’s mutual exclusion protocol and the Parallel Acknowledgment
with Retransmission that were used in prior studies. We compare state-space requirements with
one of the existing solutions DT Promela and DT Spin. With that, virtues and shortcomings of this
high-level solution are exposed. We have shown that DTMP is effective when an extensive range of
timer expiration values are used, which is usually the case in real-life SDL systems.
Ključne besede: formal specifications, formal languages, discrete time, model checking, automated extraction, SDL, Promela, SpinRCP, Sdl2pml
Objavljeno v DKUM: 27.03.2025; Ogledov: 0; Prenosov: 2
 Celotno besedilo (660,17 KB)
Gradivo ima več datotek! Več... |
2. Applying automated model extraction for simulation and verification of real-life SDL specification with spinBoštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik, 2017, izvirni znanstveni članek Opis: Formally defined Specification and Description Language (SDL) is used for the design and specification of complex safety-critical systems. Each change in the specification of the product should be immediately checked formally against the requirements’ specification. This paper presents semi-automated system abstraction, automated model extraction, simulation, and formal verification of real-life complex SDL specification. Sound algorithms implemented in our sdl2pml automated model extraction tool preserve all properties of the SDL system. Sdl2pml includes our model of discrete time, abstraction, and support for all relevant SDL functionality and constructs such as dynamic process creation, rational data types, and communication with more than one process instance. To the best of our knowledge, most of them are not supported by any other known approach. We use our SpinRCP tool for simulation and formal verification of the extracted model with the Spin model checker. We demonstrate the applicability of our approach on ISDN User adaptation protocol from SI3000 Softswitch. The extracted Promela model is the largest one ever processed by Spin. We have shown that Spin simulation and model checking can be applied successfully to such huge models.
Ključne besede: formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Objavljeno v DKUM: 03.08.2017; Ogledov: 1402; Prenosov: 435
Celotno besedilo (13,46 MB)
Gradivo ima več datotek! Več... |
3. SENZOR S KOMUNIKACIJO NFCGregor Košič, 2014, diplomsko delo Opis: V diplomskem delu je predstavljena izvedba senzorja s komunikacijo v bližnjem polju (Near Field Communication) za merjenje obratov kolesa delovnega stroja (npr. bagra). Cilj diplomskega dela je bil izdelava senzorja s komunikacijo NFC, ki beleži hitrost delovnega stroja in omogoča prikaz podatkov na pametnem telefonu ali tabličnem računalniku s podporo NFC. Naprava je opremljena s tridimenzionalnim merilnikom pospeška, oddajno-sprejemnim integriranim vezjem NFC in mikrokrmilnikom podjetja Texas Instruments, s katerim upravljamo napravo. V delu je podrobno opisano delovanje senzorja, protokol za brezžično komunikacijo v bližnjem polju, izvedba prototipa, vključno z delovanjem programske opreme.
Ključne besede: NFC, brezžična komunikacija, senzor, protokol, mikrokrmilnik
Objavljeno v DKUM: 06.03.2015; Ogledov: 2386; Prenosov: 224
Celotno besedilo (5,64 MB) |
4. ROBOT "MICROMOUSE"Marko Rman, 2011, diplomsko delo/naloga Opis: V diplomski nalogi je predstavljena izvedba robota "micromouse" za premagovanje naključnega labirinta. Cilj projekta je bila izdelava avtonomnega robota, ki je sposoben opraviti takšno nalogo. Robot je opremljen z različnimi senzorji za zaznavanje okolice, motorji za pogon, upravljanje pa se izvaja z mikrokrmilnikom podjetja Atmel. V nalogi je podrobno opisana izvedba in delovanje posameznih elektronskih delov. Predstavljeno je tudi delovanje programske opreme za izbran mikrokrmilnik.
Ključne besede: micromouse, mikrokrmilnik, optični senzor, robot
Objavljeno v DKUM: 29.09.2011; Ogledov: 2266; Prenosov: 233
Celotno besedilo (2,25 MB) |
5. BREZŽIČNI PRENOS PODATKOV MED MIKROKRMILNIKINikola Ovčar, 2011, diplomsko delo Opis: V okviru diplomskega dela smo razvili prototipni sistem za merjenje temperature in brezžični prenos podatkov s pomočjo infrardeče povezave na bazno enoto. Sistem je razdeljen na bazno enoto in več merilnih enot. Bazna enota, zgrajena okrog mikrokrmilnika PIC16F887, nadzoruje prenose iz merilnih enot ter omogoča prikaz podatkov na grafičnem zaslonu. Merilna enota je implementirana na mikrokrmilniku PIC16F88, in je zadolžena za avtomatsko zaznavanje priključenih senzorjev Dallas DS18x20 ter posredovanje podatkov na zahtevo bazne enote. Sistem samodejno zaznava število aktivnih merilnih enot in iz priključenih senzorjev pridobiva merilne podatke.
Ključne besede: mikrokrmilnik, infrardeč prenos, protokol 1-wire, temperaturni senzor, IR sprejemnik/oddajnik
Objavljeno v DKUM: 25.09.2011; Ogledov: 2441; Prenosov: 210
Celotno besedilo (2,61 MB) |
6. |
7. |
8. |
9. |
