Muutke küpsiste eelistusi

Formal Specification Level: Concepts, Methods, and Algorithms 2015 ed. [Kõva köide]

  • Formaat: Hardback, 138 pages, kõrgus x laius: 235x155 mm, kaal: 3495 g, 87 Illustrations, black and white; VIII, 138 p. 87 illus., 1 Hardback
  • Ilmumisaeg: 28-Nov-2014
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319086987
  • ISBN-13: 9783319086989
  • Kõva köide
  • Hind: 95,02 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 111,79 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
  • Formaat: Hardback, 138 pages, kõrgus x laius: 235x155 mm, kaal: 3495 g, 87 Illustrations, black and white; VIII, 138 p. 87 illus., 1 Hardback
  • Ilmumisaeg: 28-Nov-2014
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319086987
  • ISBN-13: 9783319086989

This book introduces a new level of abstraction that closes the gap between the textual specification of embedded systems and the executable model at the Electronic System Level (ESL). Readers will be enabled to operate at this new, Formal Specification Level (FSL), using models which not only allow significant verification tasks in this early stage of the design flow, but also can be extracted semi-automatically from the textual specification in an interactive manner. The authors explain how to use these verification tasks to check conceptual properties, e.g. whether requirements are in conflict, as well as dynamic behavior, in terms of execution traces.

1 Introduction
1(6)
2 Background
7(16)
2.1 Models and System States
7(5)
2.1.1 Type System
8(2)
2.1.2 Models
10(2)
2.2 Object Constraint Language
12(2)
2.2.1 Constraint Expressions
12(1)
2.2.2 Query Expressions
13(1)
2.3 Boolean Satisfiability
14(3)
2.4 Natural Language Processing
17(6)
2.4.1 Part-of-Speech Tagging
18(1)
2.4.2 Phrase Structure Trees
18(1)
2.4.3 Typed Dependencies
19(2)
2.4.4 WordNet
21(2)
3 NLP-Assisted Model Generation
23(34)
3.1 Structure Extraction
24(12)
3.1.1 Classes and Actors
24(4)
3.1.2 Attributes
28(4)
3.1.3 Operations
32(2)
3.1.4 Associations
34(2)
3.1.5 Extracting Models from the Database
36(1)
3.2 Expression Extraction
36(9)
3.2.1 Implementation
38(6)
3.2.2 Discussion
44(1)
3.3 Integrated Development Environment
45(3)
3.4 Evaluating Examples
48(6)
3.4.1 Structure Extraction
50(2)
3.4.2 Expression Extraction
52(2)
3.5 Assisted Behavior Driven Development
54(1)
3.6 Summary
54(3)
4 Verification of Static Aspects
57(52)
4.1 Static Aspects of Models
58(4)
4.2 Model Finder
62(9)
4.2.1 USE Snapshot Generator
62(2)
4.2.2 Alloy
64(4)
4.2.3 SAT Modulo Theories
68(3)
4.3 Transformation
71(24)
4.3.1 Transformation of Attributes
72(1)
4.3.2 Transformation of Links
73(3)
4.3.3 Transformation of OCL Constraints
76(11)
4.3.4 Transformation of OCL Collection Types
87(8)
4.4 Verification Tasks
95(1)
4.5 Determination of Problem Bounds
96(6)
4.5.1 Dynamic Problem Bounds
96(1)
4.5.2 Automatic Determination of Problem Bounds
97(5)
4.6 Debugging of Inconsistent Models
102(5)
4.6.1 General Debugging Flow
104(1)
4.6.2 Debugging Methods
104(3)
4.7 Test Generation for Model Transformations
107(1)
4.8 Summary
108(1)
5 Verification of Dynamic Aspects
109(22)
5.1 Dynamic Aspects of Models
111(4)
5.2 Transformation of Operation Calls
115(2)
5.3 Verification Tasks
117(4)
5.3.1 Execution Semantics
119(2)
5.4 Case Study: Invariant Elimination
121(7)
5.4.1 Problem Formulation
122(2)
5.4.2 Implementation
124(1)
5.4.3 Evaluation
125(3)
5.5 Summary
128(3)
6 Conclusions
131(2)
References 133(4)
Index 137