Formal Specification user interface for Embeded systems
Result description
The contribution focuses on user interface development for formal specifications. It describes two approaches to this toppic. First utilizes behavioral diagrams, second utilizes application source code. In both cases, the developed user interface autamatically genarates systems formal specification denoted in formal language called CSP - Communicating Sequential Processes. This notation can be verified using common model checkers. The contribution describes both, the used CSP subset, and the utilized teechniques for automated CSP generation.
Keywords
The result's identifiers
Result code in IS VaVaI
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
čeština
Original language name
Uživatelské rozhraní formální specifikace vestavěných systémů
Original language description
Práce se zabývá návrhem uživatelských rozhraní pro podporu formálních specifikací. Popisuje dva přístupy k definování formální specifikace, prvním je využití diagramu chování systému, druhým je využití zdrojového kódu aplikace. V obou případech se jednáo návrh nástroje, který automaticky vygeneruje formální specifikaci zapsanou pomocí algebry komunikujících sekvenčních procesů. Takto zapsanou formální specifikaci je následně možné verifikovat pomocí dostupných nástrojů pro verifikaci CSP. Práce definujje jak používanou podmnožinu jazyka CSP, tak i používané diagramy a přepisovací pravidla ze zdrojového kódu aplikace do CSP.
Czech name
Uživatelské rozhraní formální specifikace vestavěných systémů
Czech description
—
Classification
Type
Jx - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
GA102/02/1032: Embedded control systems and their inter-communication
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2003
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Elektrorevue - Internetový časopis (http://www.elektrorevue.cz)
ISSN
1213-1539
e-ISSN
—
Volume of the periodical
2003
Issue of the periodical within the volume
23
Country of publishing house
CZ - CZECH REPUBLIC
Number of pages
5
Pages from-to
0-4
UT code for WoS article
—
EID of the result in the Scopus database
—
Basic information
Result type
Jx - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP
JC - Computer hardware and software
Year of implementation
2003