ftp.umcs.maine.edu/2015-02-07.ftp.umcs.maine.edu.tar/ftp.umcs.maine.edu/pub/WISR/wisr6/proceedings/ascii/stillman.ascii

Text File | 1993-10-19 | 15KB | 367 lines

                       Reuse  and  Formal  Methods  for  Ada



                                            Maureen Stillman



                                    Odyssey Research Associates

                                            Ithaca, NY 14850

                                           Tel:  [phone]

                                   Email:  [e-mail]



                                                  Abstract


    We support the application of formal methods to the process of developing software. Reuse is
an important piece of this software development process. Our aim is to give softwareengineers
access  to  reusable  designs, comp onents  and  systems  developed  using  formal  methods.  This
paper describes a variety of formal methods tools and techniques, requiring different levels of
training and sophistication from their users. The result of applying these tools and techniques
will be high assurance, high quality systems composed of reusable building blocks.


Keywords: Reuse, Formal methods, Ada, Reuse libraries


Workshop Goals: To advance the state of the theory and practice combining formal methods
and reuse.


Working Groups: reuse and formal methods, reuse process models, reuse education.



                                                 Stillman- 1


1      Background



We  believe  that  trust  and  reliability  are  the  central  issues  in  reuse.  When  a  software  engineer
contemplates reuse of even the smallest fragment of code he will begin the process with uneasy and
suspicious feelings. Unanswered questions will haunt him such as:



    fflWhat is this software?


    fflWho wrote this software?


    fflWill I be sued for using this software?


    fflWill this software work the way I need it to work?


    fflWill this software work at all?


    fflHow buggy will this software be?


    fflDoes this software contain viruses?


    fflHow hard will I have to work to modify this software to do whatI want it to do?


    fflCan I really trust one or more software engineers who I don't know to write more reliable
       software than I can write myself?



In many cases, these nagging questions lead the software engineer to conclude, "I just better do it
myself.  It's safer.  It will also be a lot less work and aggravation to debug my own code than to
understand and fix someone else's code."


We believe that the use of formal methods will help mitigate some of these fears and encourage
more software engineers to attempt reuse. Software should be labeled in some way with the degree
of reliability of the code. One possibility is that the method by which the software was developed
could be described and the formal approach used (if any) would b e identified.



2      Experience  in  Reuse



ORA is  a  member  of  the  Paramax  STARS/ARPA  team.  Paramax  has  produced  a  Conceptual
Framework for Reuse Processes (CFRP) [1, 2].  ORA is also a DSSA contractor and works in the
domain of intelligent control systems [3]. We are well known for our expertise in the area of formal
methods. Our experience in the reuse area includes the verification of a number of Booch reusable
components using ORA's Penelope verification system [4].  We are currently working with NASA
and Honeywell on a Boeing 777 reuse and formal methods project in avionics. ORA is writing a
formal specification of the navigation control system.



3      Position



Our approach is to offer a range of formally based tools and techniques that are designed for use by
software engineers with different levels of sophistication and training. Each of these methods offer


                                                        Stillman- 2


increasing levels of assurance but require increased user training in exchange for greater assurance.
We  address  the  issue  of  reuse  at each  assurance  level.   Finally,  we  discuss  libraries  of  reusable
components that have different formal metho ds techniques and tools applied to them.



3.1     Lightweight Tools



The "lightweight" formal metho ds tools require little user training and no knowledge of specification
languages or proof techniques. ORA  has developed a set of these tools called AdaWise based on
our formal work in Ada semantics. The AdaWise tools, while easy to use, are rigorous because they
are based on existing formal methods technology developed at ORA. With these to ols,  we have
combined the advantages of two approaches: the precision of formal verification and the automation
of compilers.  Our tools provide the precision of formal verification without requiring the user to
write formal specifications or do proofs.  The tools automatically check any Ada program for the
presence of potential errors that typically are not detectedat compile time by a compiler.


Currently  under  development  is  an alias  checking  tool,  an  elaboration  order  checking  tool, an
incorrect  order  dependence  checker, and  a  definedness  checker.  These  AdaWise  tools  verify  a
limited  class  of  specialized  properties  for  large  programs.  These  properties  include  the  absence
of  run-time  anomalies, such  as  accessing  variables  before  they  have  been  assigned a  value,  and
independence of a program's behavior from compiler choice bychecking for erroneous executions
and  incorrect  order  dependences.  The  automatic  checks  for  these  properties  are  conservative  ,
meaning that if no warnings are issued by the tool, then the property holds, but if warnings are
issued, the property may or may not be violated.  Ifthe to ol issues a warning, it also points out
a specific region where a possible error may be. The user then has a localized region in which to
look for a violation.


These tools can address areas where subtle bugs are introduced particularly when mo difying co de
(for purposes of reuse).  For example, changing the properties of variables and violating implicit
assumptions can introduce unexpected bugs.



3.2     Middleweight Tools



"Middleweight" formal methods tools are specification languages that allow software engineers to
state properties of their design or implementation. The language we have developed is based on
Larch and is called Larch/Ada [5].  Formal sp ecification of requirements, design or code can help
users identify what the software or system is supposed to do in rigorous terms.  This will give the
software engineer a better idea of specifically what the software is intended to do.  Thus, he can
more intelligently select components for reuse andhave greater confidence in their ability to work
correctly.


These tools require educating programmers in a specification language. They would also have to
be taught how to write formal specifications.



3.3     Verification Tools



Finally, we offer a formal verification system that requires the software engineer to write specifica-
tions and do proofs. This provides the highest level of assurance, but requires significanttraining.



                                                        Stillman- 3


The user must be trained in formal specifications and must understand first order logic and be able
to guide the theorem proving system through proofs.


Our Ada verification system is called Penelope [6]. Penelope is an interactive verification CASEtool,
developed by ORA, that helps programmers develop programs and their correctness proofs from
mathematical specifications. Penelope can be used to formally verify the correctness of programs
written in a large subset of Ada.


Penelope generates a set of verification conditions (VCs) from an Ada program specified in Larch/Ada.
A proof of the VCs implies that the program meets its formal specifications.



3.4     Libraries of Components built using Formal Methods



ORA presented work on verification libraries at Tri-Ada in 1991 [7 ]. Real world software projects
will vary in their use of formal methods and some will use none.  We must generalize the idea of
verification libraries to include support for software developed with different degrees of assurance.



Background to Ada Libraries



One  of  the  design  goals  of  Ada  was  to  maintain  semantic  consistency  across  several  separately
compiled units. The Ada library was introduced to provide a repository of information about the
various units that can be accessed by the compiler.  In this way a newly compiled program will be
semantically consistent with the units currently in the library.


Program units may be changed, however, and a change may invalidate the consistency of other units.
The typical mechanism used to address this problemis to mark certain units as obsolete whenever
any  of  their  assumptions  have  changed.  An  obsolete  unit  has  to  be  recompiled.  Recompilation
constitutes a change, and so this process is transitive.


Changes  to  an  Ada  program  library  may  have  far-reaching  effects,  and  may  require  significant
amounts of recompilation.  In the case of compilation, this is only a minor problem.  In a library
where the components need to meet a high level of assurance, the traditionalobsolescence mech-
anism becomes unacceptable.  The fact that a modified piece of software now compiles does not
mean that it meets the previous level of reliability or that it now performs the new functions we
presume it will perform.



High Assurance Libraries



Formal  methods  libraries  must  deal with  reliability  problems  on  a  global  level:  the  meeting  of
previous assurance levels after the code has been modified or the design has been altered.


Superficially, the  problems  of  a  formal  methods  library  are  the  same  as  those  of  a  conventional
Ada library: in addition to static semantic consistency,we now need to be concerned with dynamic
semantic  consistency, i.e.   the  correctness  proofs.   The  details,  however,  are  quite  different.  In
addition to program objects, a high assurance library needs to deal with specifications, lemmas and
proofs.  New dependencies arise between these comp onents.  Automatic mechanisms to support a
mix of reliability levels is a topic of further research.



                                                        Stillman- 4


We advocate some way of labeling library components in ordinary libraries with some measure of
their reliability and the method used to achieve this.  This will help the software engineer in making
a decision concerning reuse. In formal methods libraries, with a fixed range of methods in use, we
can use the above techniques, with a certain amount of automated assistance, to re-establish the
original assurance level at a minimum cost.



4      Related work



Several  researchers  are  working  on connections  between  formal  methods  and  reuse  and  have  a
variety  of  approaches  [8,  9,  10].  Our  approach  is  more  low  level  than  those  cited  since  it  deals
directly with the reliability and correctness of design and co de. Cheng has done work in the area
of specifying software using a hierarchical approach.



5      Conclusions



Formal methods can be applied to systems and designs to increase system reliability.  A software
engineer's level of confidence in the correctness of other systems and components will encourage
reuse. The method used to ensure the reliability of a reusable system or component should be kept
with the system. The software engineer should restore the system to its previous level of assurance
after making modifications for reuse.



6      Bibliography



References



  [1] Software Technology for Adaptable Reliable Systems (STARS), "STARSReuse Concepts Vol-
      ume  I -  Conceptual  Framework  for  Reuse  Processes," Paramax  STARS  Technical  Report
      STARS-TC-04040/001/01, US  Air  Force  Systems  Command,  Electronic  Systems  Division,
      Hanscom Air Force Base, MA, Septemb er 1992.


  [2] Software  Technology  for  Adaptable  Reliable  Systems  (STARS),  "STARS Reuse  Concepts
      Volume  II -  Reuse  Process  Architecture," Paramax  STARS Technical  Report  STARS-TC-
      04040/002/00, US Air Force Systems Command, Electronic Systems Division, Hanscom Air
      Force Base, MA, September 1992.


  [3] D. J. H. Taylor and D. R. Platek, "Domain-Specific Software Architectures for Hybrid Con-
      trol," Sp ecial  Rep ort CMU/SEI-92-SR-9,  Carnegie-Mellon  University  Software  Engineering
      Institute, June 1992.


  [4] C.  T.  Eichenlaub,  C.  D.  Harper,  and  G.  Hird,  "Using  Penelop e  to Assess  the  Correctness
      of NASA Ada Software: A Demonstration of Formal Methods as a Couterpart to Testing,"
      NASA Contract Report 4509, Odyssey Research Associates, Inc., Ithaca, NY, May 1993.


  [5] O. R. Associates., Larch/Ada Reference Manual. Ithaca, NY, September 1989.



                                                        Stillman- 5


  [6] D. Guaspari, C. Marceau, and W. Polak, "Formal verification of Ada programs," IEEE Soft-
      ware Engineering, vol. 16, pp. 1058-1075, Sept 1990.


  [7] G. R. Hird, "Towards Reuse of Verified Ada Software," in Proceedings of Tri-Ada '90, (Ithaca,
      NY), pp. 14-21, December 1990.


  [8] M. Simos, "Towards an industry-wide consensus reuse process mo del,"  in Proceedings of the
      Fifth Annual Workshop on Software Reuse, IEEE Computer Society and University of Maine,
      1992.


  [9] J.  Knight  and  D.  M.  Kienzle,  "Reuse  of  specifications,"  in  Proceedings  of  the  Fifth  Annual
      Workshop on Software Reuse, IEEE Computer So ciety and University of Maine, 1992.


[10]  B. Cheng and J. jang Jeng, "Formal methods applied to reuse," in Proceedings of the Fifth
      Annual Workshop on Software Reuse, IEEE Computer Society and University of Maine, 1992.



7      Biography



Maureen J. Stillman is VP of Engineering at ORA Corporation. Ms. Stillman has been manager
of  the  Penelope  formal  methods  project  for  six  years.  At  ORA,  she  has  managed  a  numb er of
projects in formal methods, security, and network management.  From 1985-1987 she workedfor
Bolt, Beranek and Newman as manager of a network management project.  From 1978-1983 she
worked for MIT Lincoln Lab oratory designing network protocols for distributed mobile packet radio
networks. She received an MS in Computer Science from Northwestern University in 1985 and a
BS in Mathematics from the University of Illinoisin 1977.



                                                        Stillman- 6