mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Analyzing Industrial Simulink Models by Statistical Model Checking
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0002-5626-0587
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0002-7663-5497
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0002-4987-7669
Visa övriga samt affilieringar
2017 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose a pattern-based, execution-order preserving automatic transformation of Simulink atomic and composite blocks into stochastic timed automata that can then be analyzed formally with UPPAAL Statistical Model Checker (UPPPAAL SMC). Our method is supported by the tool SIMPPAAL, which we also introduce and apply on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

Ort, förlag, år, upplaga, sidor
Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University , 2017.
Serie
MRTC Reports, ISSN 1404-3041
Nationell ämneskategori
Teknik och teknologier Datorsystem
Identifikatorer
URN: urn:nbn:se:mdh:diva-35069ISRN: MDH-MRTC-316/2017-1-SEOAI: oai:DiVA.org:mdh-35069DiVA, id: diva2:1084738
Projekt
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyTillgänglig från: 2017-03-27 Skapad: 2017-03-27 Senast uppdaterad: 2019-05-08Bibliografiskt granskad
Ingår i avhandling
1. Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models
Öppna denna publikation i ny flik eller fönster >>Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models
2017 (Engelska)Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

Since the first lines of code were introduced in the automotive domain, vehicles have transitioned from being predominantly mechanical systems to software intensive systems. With the ever-increasing computational power and memory of vehicular embedded systems, a set of new, more powerful and more complex software functions are installed into vehicles to realize core functionalities. This trend impacts all phases of the system development including requirements specification, design and architecture of the system, as well as the integration and testing phases. In such settings, creating and managing different artifacts during the system development process by using traditional, human-intensive techniques becomes increasingly difficult. One problem stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints. Another problem is related to the fact that industrial development relies on models, e.g. developed in Simulink, from which code may be generated, so the correctness of such models needs to be ensured. A potential way to address of the mentioned problems is by applying computer-aided specification, analysis and verification techniques already at the requirements stage, but also further at later development stages. Despite the high degree of automation, exhaustiveness and rigor of formal specification and analysis techniques, their integration with industrial practice remains a challenge.

To address this challenge, in this thesis, we develop the foundation of a framework, tailored for industrial adoption, for formal specification and analysis of system requirements specifications and behavioral system models. First, we study the expressiveness of existing pattern-based techniques for creating formal requirements specifications, on a relevant industrial case study. Next, in order to enable practitioners to create formal system specification by using pattern-based techniques, we propose a tool called SeSAMM Specifier. Further, we provide an automated Satisfiability Modulo Theories (SMT)-based consistency analysis approach for the formally encoded system requirements specifications. The proposed SMT-based approach is suitable for early phases of the development for debugging the specifications. For the formal analysis of behavioral models, we provide an approach for statistical model checking of Simulink models by using the UPPAAL SMC tool. To facilitate the adoption of the approach, we provide the SIMPPAAL tool that automates procedure of generating network of stochastic timed automata for a given Simulink model. For validation, we apply our approach on a complex industrial model, namely the Brake-by-Wire function from Volvo GTT.

Ort, förlag, år, upplaga, sidor
Mälardalen University Press, 2017
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 256
Nyckelord
pattern-based formal requirements specification, formal requirements consistency analysis, formal analysis of Simulink models
Nationell ämneskategori
Teknik och teknologier Data- och informationsvetenskap
Forskningsämne
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-35085 (URN)978-91-7485-319-3 (ISBN)
Presentation
2017-04-20, Gamma, Högskoleplan 1, Västerås, 13:15 (Engelska)
Opponent
Handledare
Projekt
VeriSpec
Forskningsfinansiär
VINNOVA, 16335
Tillgänglig från: 2017-03-28 Skapad: 2017-03-28 Senast uppdaterad: 2018-01-13Bibliografiskt granskad
2. Design of Assured and Efficient Safety-critical Systems
Öppna denna publikation i ny flik eller fönster >>Design of Assured and Efficient Safety-critical Systems
2019 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

Safety-critical   systems   need   to   be   analyzed rigorously to remove software/specifications errors, that is, their requirements specifications should be unambiguous, comprehensible and consistent, and the software design should conform to the specifications, hence avoiding undesirable system failures. Currently, there is a lack of effective and scalable methods to specify and analyze requirements, and formally analyze the behavioral models of embedded systems. Most embedded systems requirements are expressed in natural language, which is flexible and intuitive but frequently ambiguous and incomprehensible.  Besides natural language, template-based requirements specification methods are used frequently to specify requirements (esp.  in safety-critical applications).  Although the latter reduce ambiguity and improve the comprehensibility of the specifications, they are usually rigid due to the constrained syntax of the templates, and template selection is challenging.  Industrial systems are frequently developed by using modeling and simulation environments such as Simulink, which is also used to generate code automatically for various hardware platforms. Therefore, it is essential to be able to formally analyze Simulink models, to get insight into the behavior of the embedded system, and also prevent potential errors from propagating into the implementation.  Analyzing the timing behavior of safety-critical software that is refined by multi-rate periodic tasks with data age constraints across the end-to-end software functionality is not trivial. This is due to the undersampling and oversampling effects caused by the data propagation from higher to lower rates and vice versa, respectively. Furthermore, when such systems are deployed on a distributed architecture, e.g., electrical/electronic vehicular system, besides assuring the timeliness, the reliability of the distributed software should be maximized to counter the higher risk of failures in the distributed computing setting, hence improving the overall predictability of the safety-critical system. However, designing for reliability usually requires additional critical system resources such as energy.  Hence, to accommodate the growing complexity of software functionality, the design of the safety-critical systems should consider the efficient use of critical system resources such as the power source, while meeting the timing and reliability requirements.

To address the above needs, in this thesis, we propose formal-methods-based approaches and optimization techniques to assure improved quality of requirements specifications and software designs, and to efficiently map software functionality to hardware. The contributions of the thesis are: (i) ReSA - a domain-specific requirements specification  language tailored to embedded systems, based on constrained natural language; (ii) a formal approach to check consistency of ReSA specifications via Boolean satisfiability problem (SAT) and ontology; (iii) a framework based on statistical model checking to analyze Simulink models via automated transformation into networks of stochastic timed automata; and (iv) a resource-efficient allocation of fault-tolerant software with end-to-end timing and reliability constraints via integer linear programming and hybrid particle-swarm optimization. Our proposed solutions are validated and evaluated on automotive use cases such as the Adjustable Speed Limiter (ASL) and the Brake-by-Wire (BBW) systems from Volvo Group Trucks Technology (VGTT), and on an Engine Management (EM) system benchmark from Bosch.

 

Abstract [sv]

Säkerhetskritiska system bör analyseras noggrant för att ta bort fel i programvaror och specifikationer, dvs systemens krav måste vara entydiga, begripliga och konsekventa, och programvarudesignen ska överensstämma med specifikationerna för att undvika oönskade systemfel. För närvarande saknas effektiva och skalbara metoder för att specificera och analysera systemkrav, och för att formellt analysera beteendemodellerna för inbyggda system. De flesta krav för inbyggda system uttrycks i naturligt språk, vilket är flexibelt och intuitivt men ofta tvetydigt och oprecist. Förutom naturligt språk används ofta mallbaserade kravspecifikationsmetoder för att specificera krav (speciellt i säkerhetskritiska tillämpningar). Även om de senare minskar otydligheten och förbättrar begripligheten, är de vanligtvis oflexibla på grund av den begränsade syntaxen i mallarna, och mallvalet är svårt. Industriella system utvecklas ofta genom att använda modellerings- och simuleringsmiljöer såsom Simulink, som också används för att generera kod automatiskt för olika hårdvaruplattformar. Därför är det viktigt att kunna formellt analysera Simulink-modeller, för att få insikt i beteendet hos det inbyggda systemet, och för att förhindra potentiella fel från att sprida sig till implementationen. Att analysera tidsperspektivet för sådan säkerhetskritisk mjukvara som har tasks med olika periodicitet och som har begränsningar på datas ålder, dvs datans färskhet, för end-to-end-programvarufunktionalitet, är inte trivialt. Detta orsakas av undersamplings- och översamplingseffekter, som uppstår när data går från högre till lägre signaleringshastigheter och vice versa. Vidare, när sådana system används i en distribuerad arkitektur, t.ex. elektriska / elektroniska fordonssystem, , så bör, förutom att säkerställa tidskraven, även tillförlitligheten hos den distribuerade mjukvaran maximeras för att motverka den högre risken för fel i den distribuerade databehandlingen, för att därigenom förbättra den övergripande förutsägbarheten för det säkerhetskritiska systemet. Design för tillförlitlighet kräver emellertid vanligtvis mer av kritiska systemresurser, såsom energi. För att tillgodose nuvarande och framtida mjukvarufunktionalitet bör utformningen av det säkerhetskritiska systemet ta hänsyn till effektiviteten hos kritiska systemresurser, såsom energiförbrukning, samtidigt som kraven på tid och tillförlitlighet uppfylls.

För att möta ovanstående behov, föreslår vi i denna avhandling formella metoder och optimeringstekniker för att säkerställa förbättrad kvalitet på kravspecifikationer och mjukvaruutveckling, och för att effektivt mappa mjukvarufunktionalitet till hårdvara. Avhandlingens bidrag är: (i) \textit{ReSA} - ett domänspecifikt språk för kravspecifikation, skräddarsytt för inbyggda system, baserat på begränsat naturligt språk; (ii) ett formellt tillvägagångssätt för att kontrollera konsistensen av \textit{ReSA}-specifikationer genom SAT och Ontologi; (iii) ett ramverk baserat på statistisk modellkontroll för att analysera Simulink-modeller via automatiserad omvandling till nätverk av stokastiska tidsautomater; och (iv) en resurseffektiv fördelning av feltolerant programvara med end-to-end-tidskrav och driftsäkerhetsbegränsningar genom heltals-linjär programmering och hybrid partikel-svärmoptimering. Våra föreslagna lösningar utvärderas i fall som används i fordon, såsom justerbar hastighetsbegränsare (ASL) och BBW-system från Volvo Group Trucks Technology (VGTT), och på ett motorstyrsystem från Bosch.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University, 2019. s. 200
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 291
Nyckelord
embedded systems design, safety critical systems, real time systems, formal method, optimization, model checking, Simulink
Nationell ämneskategori
Elektroteknik och elektronik Inbäddad systemteknik
Forskningsämne
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-43371 (URN)978-91-7485-428-2 (ISBN)
Disputation
2019-06-13, Gamma, Mälardalens högskola, Västerås, 13:15 (Engelska)
Opponent
Handledare
Projekt
VeriSpec
Forskningsfinansiär
Vinnova, 16335
Tillgänglig från: 2019-05-08 Skapad: 2019-05-08 Senast uppdaterad: 2019-05-17Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Personposter BETA

Filipovikj, PredragMahmud, NesredinMarinescu, RalucaRodriguez-Navas, GuillermoSeceleanu, Cristina

Sök vidare i DiVA

Av författaren/redaktören
Filipovikj, PredragMahmud, NesredinMarinescu, RalucaRodriguez-Navas, GuillermoSeceleanu, Cristina
Av organisationen
Inbyggda system
Teknik och teknologierDatorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 148 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf