home *** CD-ROM | disk | FTP | other *** search
/ ftp.umcs.maine.edu / 2015-02-07.ftp.umcs.maine.edu.tar / ftp.umcs.maine.edu / pub / WISR / wisr6 / proceedings / ascii / hopkins.ascii < prev    next >
Text File  |  1993-10-19  |  16KB  |  396 lines
  1.  
  2.  
  3.  
  4.  
  5.       Software  Quality  Is  Inversely  Proportional  to  Potential  Local
  6.  
  7.  
  8.                                               Verification Effort
  9.  
  10.  
  11.  
  12.                                                     John E. Hopkins
  13.  
  14.                                                    Murali Sitaraman
  15.  
  16.  
  17.  
  18.                               Department of Statistics and Computer Science
  19.  
  20.                                               West Virginia University
  21.  
  22.                                                      P. O. Box 6330
  23.  
  24.                                           Morgantown, WV 26506-6330
  25.  
  26.                                    Tel:  (304)-293-3607, fax:  (304)-293-2272
  27.  
  28.                              Email:  jhopkins@cs.wvu.edu, murali@cs.wvu.edu
  29.  
  30.  
  31.  
  32.                                                          Abstract
  33.  
  34.  
  35.            Quality and methods for measuring quality are important for all software, especially for
  36.        those that are meant to be reused. Two factors constitute the quality of a software product: (1)
  37.        Whether the product correctly meets its specification and (2) whether the product is "well engi-
  38.        neered."  Intuitively, a well-engineered component is one that is easyto comprehend, maintain,
  39.        or modify.
  40.            Software engineering literature [Pressman 92, Sommerville 89] is replete with factors and
  41.        metrics for determining how well a software product has been engineered. Unfortunately, it is
  42.        not at all clear how even a smart software designer can use these factors topro duce awell-
  43.        engineered software product.  Most published factors andmetrics are goo d only to the extent
  44.        that they can be used to argue "statistically" that one product is better than another.
  45.            In this paper, we propose a single factor for evaluating the goodness of the engineering of
  46.        a software product - the Potential Verfication Effort (PVE) involved in locally establishing the
  47.        correctness of the product.  It is possible to design software to minimize thePVE. In addition,
  48.        reduced  PVE directly  increases  most  conventionally-used  software  engineering metrics.   PVE
  49.        is not affected by whether a software product is correct or whether it is possible to establish
  50.        correctness.
  51.  
  52.  
  53.        Keywords: Reuse, software engineering, metrics, local verifiability
  54.  
  55.  
  56.        Workshop Goals: Interact; advance theory and practices of software reuse
  57.  
  58.  
  59.        Working Groups: certification, design for reuse, metrics, and reuse education.
  60.  
  61.  
  62.  
  63. ___________________________________________________
  64.      This research is funded in part by NASA Grant 7629/229/0824 and NSF Grant CCR-9204461; it has also
  65. benefitted from ARPA Grant DAAL03-92-G-0412.
  66.  
  67.  
  68.                                                         Hopkins- 1
  69.  
  70.  
  71. 1      Background
  72.  
  73.  
  74.  
  75. Over the past several years, we have been investigating various aspects of software reuse including
  76. specification of abstract functionality and performance, formal verification and testing, language de-
  77. sign, portability, distributed and real-time computing, and education. We have regularly presented
  78. papers and participated in reuse conferences and workshops, including the Annual Workshops on
  79. Software  Reuse.  Our  research  in  software  engineering  issues  at  the  West  Virginia  University  is
  80. currently funded in part by ARPA Grant DAAL03-92-G-0412, NASA Grant 7629/229/0824, and
  81. NSF Grant CCR-9204461.
  82.  
  83.  
  84.  
  85. 2      Position
  86.  
  87.  
  88.  
  89.     fflSoftware quality is inversely proportional to potential verification effort (PVE) for establishing
  90.        local correctness.
  91.  
  92.  
  93.  
  94. Sub-positions
  95.  
  96.  
  97.  
  98.     1. It is possible to design to minimize the PVE.
  99.  
  100.     2. Lower PVE improves conventional software engineering metrics.
  101.  
  102.     3. Metrics for accurately measuring PVE are likely to be different from conventional SE metrics.
  103.  
  104.  
  105.  
  106. 3      Justification  for  the  position
  107.  
  108.  
  109.  
  110. The quality of a software product can be expressed as an ordered pair:
  111.  
  112.  
  113.  
  114.     1. The "goodness" of the results
  115.  
  116.     2. The "goodness" of the product.
  117.  
  118.  
  119.  
  120. The  first  part  is  easy  to  understand  and  evaluate.   A software  product  that  generates  specified
  121. results is correct.  To determine whether a software product is correct, it can be formally verified
  122. or can be tested.
  123.  
  124.  
  125. The second part, however, is not as easy to quantify.  Software engineering literature [Pressman,
  126. Sommerville] is replete with factors and metrics for measuring this aspect of quality - determining
  127. how good a software product is or how well a software product has been engineered. Most published
  128. factors and metrics are good only to the extent that they can be used to argue "statistically" that
  129. one product is better than another. Unfortunately, it is not at all clear how even a smart software
  130. designer can use these factors to produce a well-engineered software product.
  131.  
  132.  
  133. We take the position in this paper that the potential verification effort (PVE) for evaluating part
  134. 1  (i.e., correctness)  locally  is  a  useful  factor  for  evaluating  part  2.  We  show  that  designing  to
  135. minimize PVE improves software quality and that minimized PVE directly implies improved ratings
  136. on conventional software engineering metrics.
  137.  
  138.  
  139.  
  140.                                                         Hopkins- 2
  141.  
  142. function  Max  returns  control
  143.  
  144.      parameters
  145.          preserves  x:  integer
  146.          preserves  y:  integer
  147.      ensures  "Max  iff  x >  y"
  148.  
  149.  
  150.  
  151.                                            Figure 1:  Specification of Max
  152.  
  153.  
  154. function Max(x,y) is begin if x > y then return(x) else return(y); end Max;
  155.  
  156.  
  157. function Max(x,y) is begin if x > y then return(x) else return(x); end Max;
  158.  
  159.  
  160.                                          Figure 2: Implementations of Max
  161.  
  162.  
  163.  
  164. 3.1     Independence of correctness and PVE
  165.  
  166.  
  167.  
  168. First, we define PVE. PVEis the maximum amount of effort needed to verify a product. The max-
  169. imum amount of verification effort willo ccur if apro duct iscorrect with respect to its specification.
  170. In other words, PVE is not influenced by an incorrect implementation.  An incorrect implementa-
  171. tion will be treated as if it were correct, thus yieldinga PVE rating reflecting the maximum effort
  172. necessary for verification.
  173.  
  174.  
  175. For  example, consider  the  specification  in  Figure  1  and  the  implementations  in  Figure 2.   The
  176. specification is in RESOLVE[Sitaraman 93].  Implementation 1 is correct; implementation 2 is not.
  177. With all other things for both implementations being equal, the PVErating for both procedures is
  178. the same. Implementation 1, of course, is of higher quality because it is correct. Thus, it is entirely
  179. possible that a well-engineered incorrect implementation may have a lower PVE than a correct,
  180. but poorly-engineered implementation.
  181.  
  182.  
  183.  
  184. 3.2     Example:  Lower PVE impliesformally-sp ecified, mo dular design
  185.  
  186.  
  187.  
  188. In this section, we discuss one example that demonstrates the utility of the PVE rating. We use 3C
  189. terms in this discussion, where a concept means a specification, content means an implementation,
  190. and the context is the local environment in which a concept or content is explained [Latour 90,
  191. Sitaraman  92, Tracz  90].   Given  a concept  and  a  context,  consider  the  following  four  possible
  192. contents:
  193.  
  194.  
  195.  
  196.     1. Monolithic (no components and no layering)
  197.  
  198.     2. Layered based on 1C (content-only) components
  199.  
  200.     3. Layered based on 2C (content-with-concept-only) components
  201.  
  202.     4. Layered based on 3C components
  203.  
  204.  
  205.  
  206. Let us assume that all four contents are equal onthe dimension of correctness.  However, it is clear
  207. that content 1 is poorly engineered compared to content 2 (assuming that the chosen components
  208. and the layering used in content 2 are appropriate).  Content 2 which uses a modular design without
  209. any specification is worse than content3.  "Local certifiability" [Weide 92] and hence "reusability"
  210. makes content 4 superior to content 3.  We will return to this topic later.
  211.  
  212.  
  213.                                                         Hopkins- 3
  214.  
  215.  
  216. PVE for monolithic content
  217.  
  218.  
  219. Verification  effort  in  this  case  is  a  function  of  both  the  number  of  statements  and  the  kind  of
  220. statements.  Clearly an implementation involving several loops will require more effort to verify
  221. than the one that uses only if-then-else statements which is probably more difficult to verify than
  222. one that uses no control statements.  PVE for two loops need not b e thesame either because a
  223. complex  loop  involving  a  more  complex  loop  invariant  is  harder  to  verify  than  one  that  is  less
  224. complex. In general, PVE is based on the semantics of the statements used in an implementation
  225. and the implementation. Gotos and uncontrolled use of pointers obviously increasethe PVE.
  226.  
  227.  
  228. PVE is  also  dependent  on  the  specification  for  which  the  content  is  written.  Here, we're  only
  229. comparing contents for the same specification and therefore,we can say that PVE = f(Content 1).
  230. Alternatively,PVE can also be expressed as the effort to "reverse engineer" content 1 intothe form
  231. of Content 4 (re-1-4) plus the PVE for Content 4.
  232.  
  233.  
  234. The effective PVE for monolithic content 1:  min (PVE(Content 1), re-1-4 + PVE(Content 4)).
  235.  
  236.  
  237. PVE for content layered on 1C-components
  238.  
  239.  
  240. When the sub-contents used in a content are not specified,  then verification effort is not far less
  241. than  what  is  required  in  the  monolithic  case.  Verification  here  involves  inline  code  expansion.
  242. This requires calls to subprograms, procedures, etc. to be replaced with the actual content (with
  243. proper substitutions for the calling context) during the verification process.  This means we must
  244. verify approximately the same code we did for themonolithic implementation.  In some sense, if
  245. understanding  the  bigger  content  involves  direct  understanding  of  each  of  its  constituents  then
  246. modularization is of relatively little use.
  247.  
  248.  
  249. The effective PVE for content 2: min (PVE(inline_expanded_Content 2), re-2-4 + PVE(Content
  250. 4)).
  251.  
  252.  
  253. It seems likely that re-2-4 will be smaller than re-1-4 because reverseengineering smaller modules
  254. may be inherently easier.
  255.  
  256.  
  257. PVE for content layered on 2C-components
  258.  
  259.  
  260. In  this  case, we  assume  that  the  sub-contents  have  formally-specified  concepts.  The  concept,
  261. however,  contains  only  calling  information  (such  as  the  pre-conditions  for  procedures)  etc.,  but
  262. does not include module-level context. In this case, specification-based proof rules can be used for
  263. operation calls instead of the ones requiring inline code expansion; The sub-contents themselves
  264. need to verified locally and independently to meet their specifications. This may not be possible if
  265. the context does not contain sufficient information.
  266.  
  267.  
  268. The effective PVE for content 3: min (PVE(Content 3), re-3-4 + PVE(Content 4)).
  269.  
  270.  
  271. PVE for content layered on 3C-components
  272.  
  273.  
  274. In this case, each sub-component can be locally certified to be correct [Weide 92]. Verificationeffort
  275. = PVE(Content 4) for this case is the lowest.  This verification effort will be even lower if each
  276. sub-component is a reusable component and its verifiability effort is amortized over its many uses.
  277. (Without local certifiability, reusability is impractical.)
  278.  
  279.  
  280. The effective PVE for content 4 = f(Content 4, rf) where rf is the reuse factor.
  281.  
  282.  
  283.  
  284.                                                         Hopkins- 4
  285.  
  286.  
  287. Though we have concentratedon the 3C model in this discussion, the Constraintsmo dule introduced
  288. in [Sitaraman 92] "contents layered using 4C components," can be useful in including performance
  289. issues in the PVE factor.
  290.  
  291.  
  292.  
  293. 3.3     Discussion
  294.  
  295.  
  296.  
  297. We have demonstrated a strong connection between PVE and modular design of software in this
  298. section. We believe similar results can be established for most other issues that are essential for a
  299. "well-engineered" software product.
  300.  
  301.  
  302. Metrics for PVE
  303.  
  304.  
  305. How  can  the  PVE be  measured?  Common  metrics  such  as  cyclomatic  complexity  and  lines  of
  306. code  provide  some  indication  of  the  PVE within  a  module.   Module  interaction  can  provide  a
  307. measure of PVE across modules. However, for PVE to be an accurate predictor, metrics based on
  308. formal assertions such as pre- and post-conditions of procedures, loop invariants, and semantics of
  309. statements need to designed and developed.
  310.  
  311.  
  312. Designing for lower PVE
  313.  
  314.  
  315. It is possible to design software so that its PVEis minimized, and this is an important advantage of
  316. the PVE factor. For example, Ada components designed following the guidelines in [Hollingsworth
  317. 92] will require lower PVE than ones that are not. Alternatively, adherence to guidelines such as
  318. these may provide a useful PVE metric.
  319.  
  320.  
  321. Finally, we emphasize again that PVE is independent of software correctness. PVEis a useful factor
  322. irrespective of whether verification is feasible. For a software engineer, it provides an objective that
  323. can be understood through formal training and can be followed. In the end, it is the thought (that
  324. verifiability is important) that counts!
  325.  
  326.  
  327.  
  328. 4      References
  329.  
  330.  
  331.  
  332. [Biggerstaff 89] T. Biggerstaff and A. J. Perlis, Software  Reusability, Volumes 1 and 2, Addison-
  333. Wesley,1989.
  334.  
  335.  
  336. [Hollingsworth 92] Hollingsworth, J., Software Component Design-for-Reuse: A Language-Independent
  337. Discipline Applied to Ada, Ph. D. Diss.  The Ohio State Univ., Columbus, Ohio, 1992.
  338.  
  339.  
  340. [Latour 90] Latour, L., Wheeler, T., and Frakes,W., "Descriptive and Predictive Aspects of the
  341. 3C Model:  SETA1 Working Group Summary," Third Annual Workshop:  Methods and Tools for
  342. Reuse, Syracuse, 1990.
  343.  
  344.  
  345. [Pressman  92]  Pressman,  R.  S.,  Software  Engineering:  A  Practioner's  Approach,  McGraw-Hill,
  346. 1992.
  347.  
  348.  
  349. [Sitaraman 92] Sitaraman, M., "A Unifrom Treatment of Reusability of Software Engineering As-
  350. sets," WISR'92 Proceedings, Palo Alto, CA, October 1992.
  351.  
  352.  
  353. [Sitaraman 93] Sitaraman, M., Welch, L.R., and Harms, D.E., "On Specification of Reusable Soft-
  354. ware Components," International Journal of Software Engineering and Knowledge Engineering 3,
  355.  
  356.  
  357.                                                         Hopkins- 5
  358.  
  359.  
  360. 2, World Scientific, 1993.
  361.  
  362.  
  363. [Sommerville 89] Sommerville, I., Software Engineering, 3rd ed., Addison-Westley, 1989.
  364.  
  365.  
  366. [Tracz 90] Tracz, W., "The Three Cons of Software Reuse," Third Annual Workshop:  Methods and
  367. Tools for Reuse, Syracuse, 1990.
  368.  
  369.  
  370. [Weide 92] Weide, B. W., and Hollingsworth, J., "Scalability of Reuse Technology to Large Systems
  371. Requires Local Certifiability," WISR'92 Proceedings, Palo Alto, CA,Octob er 1992.
  372.  
  373.  
  374.  
  375. 5      Biography
  376.  
  377.  
  378.  
  379. John Hopkins is a graduate student majoring in computer science at West Virginia University. He
  380. holds degrees in mathematics and computer science from West Virginia Institute of Technology. As
  381. part of the Software Reusability Groupat West Virginia University, his research interests include
  382. formal specification, formal verification, language design and software quality.
  383.  
  384.  
  385. Sitaraman is an assistant professor in computer science at the West Virginia University. He has a
  386. Ph.D. from The Ohio State University (1990). His research focuses on various aspects of software
  387. reuse and software engineering, in general. He and members of his group are currently working on
  388. specification of abstract functionality and performance, formal verification and testing, language
  389. design, portability, distributed and real-time computing, and education.  Sitaraman has authored
  390. several technical papers on related topics in software engineering.  He is amember of the ACM and
  391. IEEE Computer Society.
  392.  
  393.  
  394.  
  395.                                                         Hopkins- 6
  396.