Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Simple Homomorphism Verification Tool (SHVT) - Manual

 
: Repp, J.; Rieke, R.
: Fraunhofer-Institut für Sichere Telekooperation -SIT-, Darmstadt

:
Volltext urn:nbn:de:0011-n-473496 (2.9 MByte PDF)
MD5 Fingerprint: 9f2b22717be944317922555cc0a82fa0
Erstellt am: 30.08.2007


Element named row_ProjectData has starweb_type Output Field Repeater but ID not found in STAR Web Designer.
Darmstadt: Fraunhofer SIT, 2004, 171 S.
 
Englisch
Buch, Elektronische Publikation
Fraunhofer SIT ()

[]
Contents S.i-iii
1 Frequently Asked Questions S.1-2
- 1.1 Objects are not mouse sensitive. Only menu bars and text editor fields can be used S.1
- 1.2 Reporting Bugs S.1
- 1.3 Empty boxes instead of inscriptions are drawn after reading a drawing - S.1
- 1.4 Reporting Bugs S.1
- 1.5 Are there any example specifications available - S.1-2
- 1.6 How can I abort an arbitrary command - S.2
- 1.7 How can I stop reachability analysis - S.2
- 1.8 How can I copy selected text into a text field? S.2
- 1.9 I can?t change the size of the window for editing inscriptions? S.2
- 1.10 What is the purpose of the standard output window displayed after starting shvt? S.2
- 1.11 How can I Change Places in Glued Nets S.2
- 1.12 I have a mouse with two buttons. How can I use commands activated with the middle mouse button - S.2
- 1.13 How can I copy selected text into a text field? S.2
2 Product Net Editor S.3-20
- 2.1 Starting the Editor S.4
- 2.2 Editing a Drawing S.5
- 2.3 Correction of the Drawing S.6
- 2.4 Labelling of the Drawing S.6-10
- 2.5 Further Net Editor Commands S.10-13
- 2.6 Important Functions for a Parser Run S.14
- 2.7 Description of Parser Functions S.14-20
3 APA Editor S.21-40
- 3.1 The formal definition of APA S.22-23
- 3.2 APA Specifications S.23
- 3.3 Starting the APA Editor S.23
- 3.4 Editing a Drawing S.23-24
- 3.5 Correction of the Drawing S.25-26
- 3.6 Labelling of the Drawing S.26-29
- 3.7 Further APA Editor Commands S.29-31
- 3.8 Important Functions for a Parser Run S.32
- 3.9 Description of Parser Functions S.33-40
4 Preamble S.41-76
- 4.1 Introduction S.42
- 4.2 Data Types S.42-45
- 4.3 Functions S.45-59
- 4.4 Commentaries S.59
- 4.5 Syntax S.59
- 4.6 Input and Test of a Preamble S.60-62
- 4.7 More Examples S.62-65
- 4.8 State Transition Pattern Notation for APAs S.65-75
- 4.9 Preamble Symbols for Operators S.75-76
5 State Transition Pattern APA S.77-80
- 5.1 Creating a State Transition Pattern APA S.77-79
- 5.2 Organization of the Project Files S.79
- 5.3 Labeling of Transiton Pattern APA S.79-80
6 Syntax Checks S.81-82
- 6.1 Introduction S.81
- 6.2 Complete Syntax Check S.81
- 6.3 Partial Syntax Check S.81-82
7 Analysis S.83-120
- 7.1 Introduction S.85
- 7.2 The Analysis Window S.85-86
- 7.3 Start of the Analysis / Reduced Analysis / Simulation(Reachability Graph) S.86-88
- 7.4 General Commands S.88
- 7.5 Evaluation of the Reachability Graph S.89
- 7.6 Presentation of States S.89-91
- 7.7 Presentation of Markings S.92-94
- 7.8 Considering Abstractions and Checking Simplicity S.94-95
- 7.9 Presentation of the Minimal Automata States (Trace and Deadlock Automata) S.95-96
- 7.10 Presentation of Sets, Paths and Graphs S.96-98
- 7.11 Connected Components (Factor Graphs) S.98-100
- 7.12 Reduced Reachability Analysis S.100-102
- 7.13 Simulation S.102-103
- 7.14 Re-Directing the Print Output S.103
- 7.15 Trace Computation Reachability Graph S.103-106
- 7.16 Processing of Large Nets S.106
- 7.17 List of Analysis Commands S.106-120
8 Homomorphism Editor S.121-132
- 8.1 Introduction S.122-123
- 8.2 The Homomorphism Editor Window S.124
- 8.3 Definition Mapping for a Block S.124-128
- 8.4 Computing the Image S.128
- 8.5 Homomorphism Editor Commands S.128-132
9 Project Manager S.133-142
- 9.1 Introduction S.134
- 9.2 Create Project S.134-135
- 9.3 Editing the Project S.135
- 9.4 Usage of Preambles S.135-136
- 9.5 Commands in the Operation Menu of Tree Nodes / Edit Menu Bar S.136-140
- 9.6 Node Types in the Project Tree S.140-142
10 Temporal logic model checking S.143-171
- 10.1 Graph Construction from given TL-formula S.146
- 10.2 Examples for TL-formulae S.147-148
- 10.3 Automaton Construction from given TL-formula S.149-153
- 10.4 PLTL Satisfaction: Property as TL-formula S.154-156
- 10.5 AGEF Satisfaction: Property as TL-formula S.157-158
- 10.6 Approximate Satisfaction: Property as TL-formula S.159-162
- 10.7 Approximate Satisfaction: Property as automaton S.163-171