Transcript telaga.cs.ui.ac.id

LinguSQL – Fasilkom UI
LinguSQL
Development Tool for Reliable
Database Application
RUTI-AgI Team
Fasilkom UI
August 2005
1
LinguSQL – Fasilkom UI
Ruti-AgI Research
–
Title
AGi Research:
Developing Technology for Specifying and Generating
Critical Data Processing Programs
–
Sponsored by:
Menristek NKRI –
RUTI Batch II grant 2003-2005
–
Collaborate with:
Software Technology Group,
Utrecht University, The Netherlands
2
LinguSQL – Fasilkom UI
Ruti-AgI Fasilkom UI Team
●
Research Team
–
●
Programmer Team
(Jan-June 2005)
Heru Suhartanto
(Principle Investigator)
–
Rikky Wenang
–
L.Y. Stefanus
–
Sirajuddin Maizir
–
Belawati Wijaya
–
Budiono Wibowo
–
Siti Aminah
–
Ade Azurat
–
Jimmy
●
Programmer Team
(July-Dec 2005)
–
Carroline D. Puspa
–
Theresia Budiyanti
–
Slamet
3
LinguSQL – Fasilkom UI
Ruti-AgI Long Term Target
●
●
●
Develop Indonesia's competitive strength on software
development,
especially on the key factors: robustness and
correctness, of the software product
by applying the latest technology innovation to solve
the current problems.
4
LinguSQL – Fasilkom UI
Activities and Achievements
●
xMech - AGMech prototype (open source).
●
µPL2Java (Copyright registered).
●
Compositional implementation of programming Logic.
●
Critical module analysis of SET application (SPMB)
●
Lingu Library for HOL Theorem Prover (LinguHOL)
●
Specification of 7 critical modules of SET
●
Verification of 7 critical modules of SET in LinguHOL.
●
Lingu - Java transformer
●
Formalization of SET Problem in Atelier-B (comparative study)
5
LinguSQL – Fasilkom UI
Publication
1.
A. Azurat, et al. Towards Automated Verification of Database Scripts. TPHOLS, UK 2005.
2.
B. Wibowo, R. Wenang, & S. Maizir. LinguSQL: A Verification and Transformation Tool for Lingu. SNIKTI, 2005.
3.
J. Bong, & H. Suhartanto. Penerjemah MuPL2Java: Transformasi Bahasa Spesifikasi ke Bahasa Pemrograman. SNIKTI, 2005.
4.
H. Suhartanto, et al. Technology for Specifiying and Generating Critical Data Processing Programs. QIR, 2005.
5.
R. Wenang, et al. LinguSQL: A Verification and Transformation Tool for Database Application.
6.
I.S.W.B. Prasetya, et al. Building Verification Condition Generators by Compositional Extensions. IEEE-SEFM, German, 2005.
7.
I.S.W.B. Prasetya, A. Azurat, T.E.J. Vos, A. van Leeuwen, H. Suhartanto, Theorem Prover Supported Logics for Small Imperative
Languages, Institute of Information and Computing Sciences, Utrecht University, 2005.
8.
J. Bong & H. Suhartanto, Penerapan Attribute Grammar dalam Penerjemahan Bahasa Spesifikasi Lingu ke Bahasa Pemrograman
Java, KNSI 2006 Bandung.
9.
J. Bong, Pengembangan Penerjemah Lingu ke Java dengan Attribute Grammar, Master Thesis, Faculty of Computer Science UI
2006.
10. S. Aminah, Penerapan Formal Method pada study kasus SPMB dengan Atelier-B, Master Thesis, Faculty of Computer Science UI
2006.
11. T. Budiyanti, Pengembangan Software dengan Refinement Menggunakan Metode B, KNSI Bandung 2006
12. C. D. Puspa, Implementasi Prototype Lingu (Little Language) pada Studi Kasus SPMB, KNSI Bandung 2006
6
LinguSQL – Fasilkom UI
Problem Statement
●
●
Critical software requires intensive formal testing and
verification,
–
difficult
–
expensive
Legacy code
–
dynamic technology
–
static functional specification
–
re-usability vs re-engineering
7
LinguSQL – Fasilkom UI
State of the Art
●
Reliable software
–
open problem
–
complexity, undecidability
● state explosion problem
domain specific solution
●
Program Transformation
–
on demand, specific
–
costly
academic tool
●
hardware verification
Required highly qualified
expertises:
➔
●
–
●
●
Stratego, Utrecht
Netherlands
no integration with reliable
software development
●
–
NASA
Intel
8
LinguSQL – Fasilkom UI
What is Lingu?
●
A Lightweight language to program data
transformation on database integrated with verification
and formal testing .
●
Domain Specific Language
●
High level Language.
●
No optimization features (e.g. No Arrays nor pointer).
●
Small. Limited constructs
(e.g. no String[n] nor sort by modifier)
9
LinguSQL – Fasilkom UI
What is LinguSQL?
LinguSQL:
IDE
(Integrated Development Environment)
for
reliable database application.
10
LinguSQL – Fasilkom UI
Why Research ?
●
open problem
–
●
some technical issues are debatable subjects
experimental tool
–
additional analysis for the open problem.
11
LinguSQL – Fasilkom UI
Related work
●
Comparison study with B (Atelier-B)
–
B is a method, theory & language, developed by Abrial
–
It is supported by commercial tools (Atelier B & B-ToolKit)
–
It is used by many industries (MATRA, IBM, Siemens)
–
Software development with B starts from creating abstract
models, then refine them into concrete models
– Refinement is central of B method
–
All of the B components are written using Abstract
Machine Notation (AMN)
12
LinguSQL – Fasilkom UI
SET implementation in B
●
●
●
B is general formal method, not specially dedicated
for data processing problem
B method lacks the abstraction mechanisms
supported by the database conceptual languages
Problems in the SET implementation:
–
●
What is a proper abstraction for database structure like
records?
Solution
–
Record is modeled as constant mapping
13
LinguSQL – Fasilkom UI
SET implementation in B (cont.)
●
●
●
●
Records of data is modeled as set
Field of record is modeled as function from set of records to
other set which become field type.
With this approach, abstract machines are directly refined to
implementation machines using some library machines
This approach can be adopted by other data processing
problems
14
LinguSQL – Fasilkom UI
Comparison Result
●
Atelier B
–
Take some time to understand the concept and the tool
–
Difficult to prove
–
Too much detail
–
Low level verification
15
LinguSQL – Fasilkom UI
Comparison Result (summary)
16
LinguSQL – Fasilkom UI
LinguSQL: The Innovation
●
●
The use of Lingu language and program transformation
technology based on Attribute Grammar
The application of higher order logic on program
verification especially on database application.
17
LinguSQL – Fasilkom UI
LinguSQL: Features
●
●
●
Code Transformation from Lingu to Java
Formal program verification with theorem prover (HOL)
support for database application
Integrated testing with sample data generator. Tester
should only list the scenario to be tested.
18
LinguSQL – Fasilkom UI
Translator Lingu to Java
●
Background
–
Legacy code
●
●
–
Programming language emerge quickly. The availability of old
language programmer is low.
Re-engineering in new programming language has high risk of
error.
Alternative Solution
●
Translate the program directly by automatic tool.
19
LinguSQL – Fasilkom UI
Progress
●
●
MuPL2Java
–
Translate MuPL (Lingu's early version) in to Java
–
Development of automatic tool using JavaCUP
Tranlator Lingu to Java
–
Part of LinguSQL
–
Development of automatic tool using JavaCC
20
LinguSQL – Fasilkom UI
Translator Lingu to Java
●
Result
–
Lingu Program is represented as data structure in UUAG.
–
Using combinatoric tecnology of Parser and scanner in
Haskell
–
Semantic translation using pretty printing library in UUAG
–
Has been used in SET case study.
21
LinguSQL – Fasilkom UI
LinguSQL: The Advantages
●
one source code written in high level language for
several executable code.
●
Testing Scenario
●
integrated Theorem prover interface
●
integrated testing with generated sample data
22
LinguSQL – Fasilkom UI
LinguSQL for APICTAN
●
●
●
Improve the quality of APICTAN's software product
Eliminate future legacy code problem and efficient
investment of software
Technological leap as one of the key success factors to
compete in the global market of software and
information technology
23
LinguSQL – Fasilkom UI
Status
●
Prototype – used only on specific domain problem.
●
Copy right registered
●
●
Seven (7) Critical modules on SET application has
been verified and generated (Java code).
Some expected features are not completed yet,
especially on domain specific data sample generator
24
LinguSQL – Fasilkom UI
LinguSQL Alpha 0.1
25
LinguSQL – Fasilkom UI
Run Test Scenario
26
LinguSQL – Fasilkom UI
Verification- Proof check
27
LinguSQL – Fasilkom UI
Transform Lingu to Java
28
LinguSQL – Fasilkom UI
Future Work
●
●
next 6 months
–
additional proof-library
–
better user interface
●
next 12 months
–
–
–
complete support on
database test generator
more examples on database
application
some technical reports
●
next 18 months
(beta version)
–
support for more general
application
–
comprehensive reference
manual
next 24 months
(commercial product)
–
transformation to other
languages (C++, Ada)
–
more examples
29