[comp.specification] Z, VDM and non-functional requirements

krees@axion.bt.co.uk (Kearton Rees) (06/19/91)

Does any one have (or know of) information on how
Z and VDM handle non-functional requirements?

(By non-functional requirements I mean attributes like ease of use,
performance, ease of maintenance, availability, security, reliability etc.)

Kearton

#---------------------------------------------------------------#
 Kearton Rees				    krees@axion.bt.co.uk
 Software Technology Division,   British Telecom Research Labs.,  
 Martlesham Heath,  Ipswich,  Suffolk, IP5 7RE   United Kingdom.	
#---------------------------------------------------------------#

wallace@shodha.enet.dec.com (Richard Wallace) (06/20/91)

In article <1991Jun19.143628@axion.bt.co.uk>
Kearton Rees (krees@axion.bt.co.uk) writes:

>Does any one have (or know of) information on how
>Z and VDM handle non-functional requirements?

I really don't know how you would resolve the oxymoron of "non-functional
requirements."  Could it be that you are looking for subjective
intangables such as beauty, goodness, etc.?

A system, and specifically any system that has software in it, has to have
each requirement to be a functional one by definition.  If it isn't
a function of the system, then it isn't a requirement on the system.

>(By non-functional requirements I mean attributes like ease of use,
>performance, ease of maintenance, availability, security, reliability etc.)

Can't "ease of use" be futher broken down into specifications for:
	* number of operations per function
	* logical flow of commands
	* handling of errors

Can't "availabiltiy" be sepcified by a specification of time for the
system to be operational (auditing software does this already so I
don't see why this can't be specified in Z).  "Reliability" is done in
the same vein with checksums or some other validation criteria.

I know that security CAN be stated as a functional requirement (in Z)
as I've done it for Digital for our customer (the U.S. Air Force).

"Maintenance" is a bit more intangible than the rest, but it can be
formally specified by using a Delta schema to specify the operations
for mean time to repair.  This schema would be loosely bound with the
system of interest.

I would maintain that if it can be quantified, it can be specified.
This topic could become philosophica! 8-)

Richard 
+-------------------------------------------------------------------+
Richard Wallace                         wallace%cookie@decpa.dec.com
Digital Equipment Corporation
1175 Chapel Hills Dr.
Colorado Springs, CO  80920 U.S.A.
+-------------------------------------------------------------------+