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 Science
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: 2013-03-26

Open Access in DiVA

fulltext(250 kB)103 downloads
File information
File name FULLTEXT01.pdfFile size 250 kBChecksum MD5
1e647f11a2e1ac17597939dada2aa9988233f3032321552bc1aeff61313b083a2608ac43
Type fulltextMimetype application/pdf

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 103 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

Total: 145 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