his.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Verifying an industrial system using REX
University of Skövde, School of Humanities and Informatics.
2008 (English)Report (Other academic)
Abstract [sv]

Användandet av formella metoder för att höja kvalitén på mjukvara används inte i någon stor utsträckning inom industrin. Vi hävdar att användandet av ett verktyg där man kan specificera sitt system i ett högnivåspråk istället för direkt i det formella språket är en möjlig väg för att förse mjukvaruutvecklare med kraftfulla verifieringsverktyg som är specifika för olika paradigmer. Verktyget REX stödjer specifikation av applikationer specificerade som en mängd regler och sammansatta händelser. Dessutom tillhandahåller REX stöd för att överföra regelbaserade modeller och applikations specifika krav från REX till det formella verktyget Uppaal. Model-checkern i Uppaal kontrolleras automatiskt av REX. I denna rapport presenteras en fallstudie där ett system som används för att planera produktionen på Volvo IT i Skövde har specificerats som regler och verifierats formellt med hjälp av REX. Syftet med fallstudien är att visa att REX kan användas för att specificera och verifiera ett komplext system som används i verkligheten.

Abstract [en]

The use of formal methods for enhancing software quality is still not used in its full potential in industry. We argue that seamless support in a high-level specification tool is a viable way to provide industrial system designers with complex and powerful formal verification techniques.

The REX tool supports specification of applications constructed as a set of rules and complex events. REX provides seamless support for specifying and verifying application specific requirement properties in the timed automata model-checking tool Uppaal. The rules, events and requirements of an application design is automatically transformed to a timed automaton representation and verified in the Uppaal tool.

In order to validate the applicability of our approach, we present experimental results from a case-study of an industrial system. Based on the case-study results, we conclude that complex applications can be efficiently verified using our approach.

Place, publisher, year, edition, pages
Skövde: Institutionen för kommunikation och information , 2008. , 45 p.
Series
IKI Technical Reports, HS-IKI-TR-08-001
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:his:diva-1284OAI: oai:DiVA.org:his-1284DiVA: diva2:2422
Available from: 2008-06-17 Created: 2008-06-17 Last updated: 2018-01-13

Open Access in DiVA

fulltext(250 kB)114 downloads
File information
File name FULLTEXT01.pdfFile size 250 kBChecksum SHA-1
2321552bc1aeff61313b083a2608ac431e647f11a2e1ac17597939dada2aa9988233f303
Type fulltextMimetype application/pdf

Authority records BETA

Ericsson, AnnMarie

Search in DiVA

By author/editor
Ericsson, AnnMarie
By organisation
School of Humanities and Informatics
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 114 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 153 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf