Document

Transcript Document

Formal Specification of Non-Functional Aspects
in Two-Level Grammar
Chunmin Yang, Beum-Seuk Lee, Barrett Bryant,
University of Alabama at Birmingham
Carol Burt
Rajeev Raje
Indiana University Purdue University Indianapolis
Mikhail Auguston Andrew Olson
New Mexico State University
This research is based upon work supported by, or in part by, the U. S. Army Research Laboratory
and the U.S. Army Research Office under contract/grant number DAAD19-00-1-0350 and by the U. S.
Office of Naval Research under award number N00014-01-1-0746.
Contents
Motivation
Approach
Problem Statement
Objectives
System Structure
Non-Functional Aspect (QoS)
Natural Language Processing
Knowledge Base
Two-Level Grammar (TLG)
Case Study – ATM Example
Conclusion
2
Problem Statement
Functional aspect
Non-functional aspect
Well defined domain (concrete)
Abstract and non-quantifiable
Local and simple attributes correlation
Dynamic and complex correlation
Easy prototyping and verification
Poor measurement and formalism
Users’ main interest
Its importance neglected
“the system should sort the list of the
given numbers”
“the system should maintain high
level of security”
Non-functional aspect (Quality of Service - QoS) in the UniFrame project
Query of heterogeneous components that satisfy certain QoS
QoS specification and management
3
Objectives
Formal specification of QoS
Decomposability of QoS attributes
Correlation among QoS actions
Two-level Grammar (TLG)
QoS specifications in natural language
User friendly interface
Reuse of requirements document
Natural Language Processing (NLP)
4
System Structure
QoS Requirements Document in NL
Informal
QoS Requirements Document in XML
Natural Language Processing
Knowledge Base
Decontextualization
Two Level Grammar
Data and Function translation
Vienna Development Method
IFAD VDM Tool Kit
Formal
Code generators
Java, C++
Rose-VDM Link
UML
Interpreter
5
Non-functional Aspect (QoS)
QoS attributes
Features or parameters of QoS
QoS catalog : throughput, capacity, end-to-end delay, parallelism constraints,
availability, ordering constraints, error rate, security, transmission, adaptivity,
evolvability, reliability, stability, result, achievability, priority, compatibility, and
presentation
Decomposition
QoS actions
Events that have affect on QoS attributes
Correlation
QoS properties
Constraints on QoS actions
6
Natural Language Processing
QoS Description
Syntax
Level
Part of Speech Parsing
Part of Sentence Parsing
Pragmatics
Level
Context
Semantics
Level
Pronouns
Knowledge Base
7
Natural Language Processing (Cont’d)
Sentence
Noun_Phrase
Pronoun
Verb_Phrase
Verb
Propos_Phrase
Proposition
time
flies
Subject
Verb
like
Proposition
Noun_Phrase
Article
Noun
an
arrow
Modifier
Prop_Object
8
Knowledge Base
Composed of
Linguistics information – parts of speech
Contextual information – relations between sentences
Tree-like structure
Example
Encrypt ion byt e lengt h
update level
ATM
be 6
Maximum allowed at t empt s
System
be less than 5
be 80% secure
Account type be a savings account
Security
Maximum connect ions of bank
update attributes
Delay level
be less than 50
be less than 50
Maximum allowed attempts
be limited to 4
9
Two-Level Grammar (TLG)
Syntax
class Class_Name.
Data_Name {, Data_Name} :: Data_Type {, Data_Type}.
Rule_Name : Rule_Body {, Rule_Body} {; Rule_Body}.
end class.
Properties
Natural-language-like syntax
Flexibility
Formal notation
Formalism
Object-oriented structure
Abstraction
Logic/Functional operation
Computation
10
Two-Level Grammar - Example
class Palindrome.
Char :: Character.
Str :: {Char}*.
Empty is a palindrome.
Char is a palindrome.
Char Str Char is a palindrome : Str is a palindrome.
end class.
11
ATM – QoS Requirements Document in NL
ATM's security property is as follows.
The length of the encryption byte should be bigger than 3 and the allowed
attempts has to be smaller than the maximum allowed attempts.
If the encryption byte length is 6 and the maximum allowed attempts is less
than 5 then the system is 80% secure.
If the account type is a savings account or the maximum allowed connections
of the bank is less than 50 or the delay level is less than 50 then the maximum
allowed attempts is limited to 4.
If the user timeout is between 10000 and 120000 milliseconds we have a good
delay level.
If the response time is longer than 30000 milliseconds, the delay level drops
down to 40%.
12
ATM – QoS Requirements in XML
<c title = "ATM">
<c title = "Security">

<s>The length of the encryption byte should be bigger than 3 and the allowed
attempts has to be smaller than the maximum allowed attempts</s> 

<s>If the encryption byte length is 6 and the allowed attempts is less than 5 then the
system is 80% secure</s> 

<s>If the account type is a savings account or the maximum allowed connections of
the bank is less than 50 or the delay level is less than 50 then the maximum allowed
attempts is limited to 4</s> 
</c>
<c title = "Delay">

<s>If the user timeout is between 10000 and 120000 milliseconds we have a good
delay level</s> 

<s>If the response time is longer than 30000 milliseconds the delay level drops down to
40%</s> 
</c>
</c>
13
ATM - Knowledge Base
Length of encryption byte
satisfaction check
Allowed attempts be smaller than Maximum allowed attempts
Encryption byte length
Security
update level
be bigger than 3
be 6
Maximum allowed attempts
System
be less than 5
be 80% secure
Account type be a savings account
Maximum connections of bank
ATM
update attributes
Delay level
be less than 50
Maximum allowed attempts
satisfaction check
Delay
update level
User timeout
have
be less than 50
be limited to 4
be between 10000 and 120000 milliseconds
Good delay level
Response time
Delay level
be longer than 30000 milliseconds
drop down to 40%
14
ATM – Two-Level Grammar (TLG)
class Property.
Level :: int.
end class.
class Bank_Capacity extends Property.
Maximum_Connections :: Integer.
end class.
class ATM_Delay extends Property.
Response_Time :: Integer.
User_Timeout :: Integer.
check satisfaction :
User_Timeout > 10000, User_Timeout < 120000.
update level :
Response_Time > 30000, Level := 40.
end class.
15
ATM – Two-Level Grammar (cont’d)
class ATM_Security extends Property.
Maximum_Allowed_Attempts :: Integer.
Encryption_Byte_Length :: Integer.
Allowed_Attempts :: Integer.
Account_Type :: String.
check satisfaction :
Encryption_Byte_Length > 3, Allowed_Attempts < Maximum_Allowed_Attempts.
update level :
Encryption_Byte_Length = 6, Allowed_Attempts < 5,
Level := 80.
update attributes :
Account_Type = "savings", Maximum_Allowed_Attempts := 4;
Bank_Capacity Maximum_Connections < 50, Maximum_Allowed_Attempts := 4;
ATM_Delay Level < 50, Maximum_Allowed_Attempts := 4.
end class.
16
ATM - Unified Modeling Language (UML)
17
Conclusion
Summary
Formal specification of QoS using TLG
QoS specifications in natural language using NLP
Future Work
Express the constraints in Object Constraint Language (OCL)
Combine Model Driven Architecture (MDA) and formal methods in
representing the QoS properties, and implement the representation
within MDA
18
THE END
Contact info :
Beum-Seuk Lee : [email protected]
www.cis.uab.edu/info/grads/leebs
UniFrame
: www.cs.iupui.edu/uniFrame

Document

Transcript Document

Directory