Sökning: WFRF:(Rodriguez Navas Guillermo)
> (2015-2019) >
Ontology-based Anal...
Ontology-based Analysis and Scalable Model Checking of Embedded Systems Models
-
- Mahmud, Nesredin (författare)
- Mälardalens högskola,Inbyggda system,Formal Modeling and Analysis of Embedded Systems
-
- Seceleanu, Cristina, Associate Professor (preses)
- Mälardalens högskola,Inbyggda system
-
Ljungkrantz, Oscar (preses)
-
visa fler...
-
Rodriguez-Navas, Guillermo (preses)
-
- Scandariato, Riccardo, Associate Professor (opponent)
- Chalmers University of Technology, Sweden
-
visa färre...
-
(creator_code:org_t)
- ISBN 9789174853377
- Västerås : Mälardalen University, 2017
- Engelska 200 s.
- Relaterad länk:
-
https://mdh.diva-por... (primary) (Raw object)
-
visa fler...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- Currently, there is lack of effective and scalable methods to specify and ana-lyze requirements specifications, and verify the behavioral models of embed-ded systems. Most embedded systems requirements are expressed in naturallanguage which is flexible and intuitive but frequently ambiguous, vague andincomprehensive. Besides to natural language, template-based requirementsspecification methods are used to specify requirements specifications (esp. insafety-critical applications), which reduce ambiguity and improves the com-prehensibility of the specifications. However, the template-based method areusually rigid due to the fixed structures of the templates. They also lack meta-models for extensibility, and template selection is challenging.In this thesis, we proposed a domain specific language for embedded sys-tems, called ReSA, which is constrained natural language but flexible enoughto allow engineers to use different constructs to specify requirements. Thelanguage has formal semantics in proportional logic and description logic thatenables non-trivial and rigorous analysis of requirements specification, e.g.,consistency checking, completeness of specifications, etc.Moreover, we propose a scalable formal verification of Simulink models,whichisusedtodescribethebehaviorofsystemsthroughcommunicatingfunc-tional blocks. In industry, Simulink is the de facto modeling and analysis en-vironment of embedded systems. It is also used to generate code automati-cally from special Simulink models for various hardware platforms. However,Simulink lacks formal approach to verify large and hybrid Simulink models.Therefore, we also propose a formal verification of Simulink models, repre-sented as stochastic timed automata, using statistical model checking, whichhas proven to scale for industrial applications.We validate our approaches on industrial use cases from the automotiveindustry. These includes Adjustable Speed Limiter (ASL) and Brake-By-Wire(BBW) systems from Volvo Group Trucks Technology, both safety-critical.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
Nyckelord
- requirements specification
- embedded systems
- ontology
- formal methods
- simulink
- sat
- domain specific language
- requirements boilerplates
- Computer Science
- datavetenskap
Publikations- och innehållstyp
- vet (ämneskategori)
- lic (ämneskategori)
Hitta via bibliotek
Till lärosätets databas