source: CIVL/src/overview.html@ f6ce0eb

1.23 2.0 main test-branch
Last change on this file since f6ce0eb was 16dc0b6, checked in by Manchun Zheng <zmanchun@…>, 12 years ago

changes from code review meeting on May 22, 2014.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@1052 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 4.9 KB
Line 
1
2<html>
3<body>
4
5 <p>Welcome to CIVL, the Concurrency Intermediate Verification
6 Language tool. CIVL is a Java project for verifying concurrent
7 programs written in CIVL-C, which is a C dialect with extensions to
8 concurrent language constructs. The CIVL project uses ABC, SARL and
9 GMC. The CIVL tool can be used to perform a number of tasks, including
10 the following:
11 <ol>
12 <li>preprocess or pass a CIVL-C program;</i>
13 <li>verify a CIVL-C program;</li>
14 <li>run a CIVL-C program;</li>
15 <li>replay traces for a program.</li>
16 </ol>
17
18 In addition, it provides a framework for developing your own libraries
19 or transformations on ASTs of various language extensions and
20 libraries.
21 </p>
22
23 There is a simple command-line interface for CIVL (see {@link
24 edu.udel.cis.vsl.civl.CIVL CIVL}), but most users will want to use CIVL
25 through the user interface (see {@link
26 edu.udel.cis.vsl.civl.run.IF.UserInterface UserInterface}). To use the
27 API, it is helpful to have some understanding of the modular structure
28 of CIVL. The CIVL source code is decomposed into modules, each with a
29 well-defined interface and set of responsibilities. Some of these
30 modules are decomposed further into sub-modules. The top-level modules
31 are:
32 <ol>
33
34 <li><strong>util</strong>
35 <ol>
36 <li>responsibilities: simple general-purpose utility classes
37 that do not use other parts of CIVL</li>
38 <li>uses: nothing</li>
39 <li>interface: {@link edu.udel.cis.vsl.civl.util.IF}</li>
40 <li>entry point: none</li>
41 </ol></li>
42
43 <li><strong>config</strong>
44 <ol>
45 <li>responsibilities: static configurations of the system</li>
46 <li>uses: <strong>gmc</strong></li>
47 <li>interface: {@link edu.udel.cis.vsl.civl.config.IF}</li>
48 <li>entry point: CIVLConfiguration</li>
49 </ol></li>
50
51 <li><strong>transform</strong>
52 <ol>
53 <li>responsibilities: transformations of an AST</li>
54 <li>uses: <strong>abc</strong>, <strong>sarl</strong></li>
55 <li>interface: {@link edu.udel.cis.vsl.civl.transform.IF}</li>
56 <li>entry point: CIVLTransform</li>
57 </ol></li>
58
59 <li><strong>model</strong>
60 <ol>
61 <li>responsibilities: definitions of the control flow graph
62 representation of a CIVL-C program</li>
63 <li>uses: <strong>util</strong>, <strong>config</strong>, <strong>abc</strong>,
64 <strong>gmc</strong>, <strong>sarl</strong></li>
65 <li>interface: {@link edu.udel.cis.vsl.civl.model.IF}</li>
66 <li>entry point: Models</li>
67 <li>submodules
68 <ol>
69 <li><strong>expression</strong>
70 <ol>
71 <li>responsibilities: definitions of various expressions of
72 CIVL</li>
73 <li>interface: {@link
74 edu.udel.cis.vsl.civl.model.IF.expression}</li>
75 <li>entry point: none</li>
76 </ol></li>
77 <li><strong>location</strong>
78 <ol>
79 <li>responsibilities: definitions a location in the control
80 flow graph of a CIVL-C program</li>
81 <li>interface: {@link
82 edu.udel.cis.vsl.civl.model.IF.location}</li>
83 <li>entry point: none</li>
84 </ol></li>
85 <li><strong>statement</strong>
86 <ol>
87 <li>responsibilities: definitions of various statements of
88 CIVL</li>
89 <li>interface: {@link
90 edu.udel.cis.vsl.civl.model.IF.statement}</li>
91 <li>entry point: none</li>
92 </ol></li>
93 <li><strong>type</strong>
94 <ol>
95 <li>responsibilities: definitions of various types of CIVL</li>
96 <li>interface: {@link edu.udel.cis.vsl.civl.model.IF.type}</li>
97 <li>entry point: none</li>
98 </ol></li>
99 <li><strong>variable</strong>
100 <ol>
101 <li>responsibilities: definitions of a variable of CIVL</li>
102 <li>interface: {@link
103 edu.udel.cis.vsl.civl.model.IF.variable}</li>
104 <li>entry point: none</li>
105 </ol></li>
106 </ol>
107 </li>
108 </ol></li>
109
110 <li><strong>state</strong>
111 <ol>
112 <li>responsibilities: creation and manipulation of states of a CIVL model.</li>
113 <li>uses: <strong>config</strong>, <strong>model</strong></li>
114 <li>interface: {@link edu.udel.cis.vsl.civl.state.IF}</li>
115 <li>entry point: States</li>
116 </ol></li>TBC.
117
118 <li><strong>run</strong>
119 <ol>
120 <li>responsibilities: parsing command line inputs and initial
121 configurations of the tool</li>
122 <li>uses: <strong>err</strong>, <strong>kripke</strong>, <strong>model</strong>,
123 <strong>state</strong>, <strong>transform</strong>, <strong>util</strong>,
124 <strong>abc</strong>, <strong>gmc</strong>, <strong>sarl</strong></li>
125 <li>interface: {@link edu.udel.cis.vsl.civl.run.IF}</li>
126 <li>entry point: UserInterface</li>
127 </ol></li>
128
129 <li><strong>main</strong>
130 <ol>
131 <li>responsibilities: parsing command line inputs and initial
132 configurations of the tool</li>
133 <li>uses: <strong>run</strong></li>
134 <li>interface: {@link edu.udel.cis.vsl.civl}</li>
135 <li>entry point: CIVL</li>
136 </ol></li>
137
138 </ol>
139
140</body>
141</html>
142
Note: See TracBrowser for help on using the repository browser.