GDLN Learning Activity Development (GLAD) Batch 3
A FORMAL METHOD APPROACH
FOR RELIABLE AND HIGH QUALITY SOFTWARE
Inception ProposalReport
Principal investigator: Heru Suhartanto, PhD
Faculty of Computer Science
University of Indonesia
Directorate of General Higher Education
Ministry of National Education
2007GDLN Learning Activity Development (GLAD) 2007
Batch 3
Revised Proposal
A FORMAL METHOD APPROACH
FOR RELIABLE AND HIGH QUALITY SOFTWARE
Coordinator: Heru Suhartanto, PhD
Faculty of Computer Science
University of Indonesia
Directorate General of Higher Education
Ministry of National Education
2007
A. Executive summary
Software is becoming one of the daily need in this computerize world. The quality of the software relies heavily on its engineering process. Some of the local software need has been developed locally. Although the software development in Indonesia is cheaper than in most other countries, unfortunately those software products are unlikely to be marketed internationally due to its quality. The current state of the art of software engineering in Indonesia is quite far behind the international onestate of the art. One of the current approaches that we would like to raise is the use of formal method for software engineering.
The proposed learning activity is trying to bring the latest state of the art of a reliable software engineering to Indonesia academicians and software engineers. We have experience on doing research in this area, and we would also like to disseminate our research. We have conducted a three years research in this area in collaboration with UtrechtUniversity. As one of the result of this research collaboration is a prototype tool name LinguSQL. This tool represents the state of the art in the software development of database applications. We would like to introduce the audience and prepare them to be able to use this tool to improve the quality and the reliability of the software they develop. With this improvement, we expect to bring Indonesian software product into international market.
We plan to have a one day two daysseminar preceded by one-week online independent learning and discussion on the required basic knowledge of formal method to provide the audiences with sufficient pre-knowledge to be able to understand the latest approach. Sufficient hand-out in the forms of hard-copy and in the form of e-learning material via the internet will be provided to the audiences well before the seminar to prepare them with the material in advance.
B. Background information
In the information era, many human tasks have been replaced by computer systems. The number of existing application programs grows very quickly. Industrial companies and other institutions often need to change their computer system as the complexity of their problem increases. The need to modernize legacy software system is primarily driven by three factors: expansion of the system’s functionality; improved maintainability offered by newer tools and techniques; and reduction of operational costs and improved reliability offered by new hardware [Tsr02].
Reliability of a program based on mathematical proof was raised since late 60's by Floyd and Hoare [Hoa69]. They introduced the assertion of simple triple which is known as Hoare triple. The triple consists of pre-condition, program statement and post-condition. It is denoted as {P} S {Q}. The triple means that if the pre-condition P holds in the beginning of S, then after the execution of S terminate the condition Q will hold. The idea has not gained popularity until the success of mathematical reliability proof on hardware with the help of computer program called theorem prover. This emerging approach is not meant to replace the software quality procedure of testing. It is meant to complement it since no matter how intensive the testing is, it would not be able to show the absence of error as Dijkstra[Dij72] said:
”... program testing can be a very effective way to show the presence of bugs,
but is hopelessly inadequate for showing their absence.”
One of the difficulties inof doing verification for software is the readability of its specification. Before doing verification, we first need to specify the expected behavior of the program. Using common natural language has been proven not sufficient, due to its natural ambiguity. The use of a mathematical style of language provides a precise expression, but reading it will be difficult. Due to the high complexity of practical cases, it is not even visible by human eyes to render those expressions to check if they really express the expected behavior. The next step after having a formal written specification of a program, we have to define a way to verify if the implemented program complies with the defined specification. The approach to guarantee the reliability of a program is called program verification. Another approach which is trying to generate a correct program from the given specification is called program refinement. Both approaches require a mean to do reasoning. The reasoning is necessary to provide justification of the steps to refine a specification or to justify if a program complies with its specification. Since the specification is sometimes difficult to be read, the reasoning of a specification and its program can also be very delicate. It uses so many variables in which for real application would be difficult for any human to follow. The need of machine help becomes obvious, not only for efficiency but also for feasibility.
Unfortunately the Indonesian Software Engineering's state of the art is still quite far from adopting this concept. The Faculty of Computer Science University of Indonesia has conducted a research in this area in collaboration with UtrechtUniversity[HPA06]. We have created a prototype tool name LinguSQL[APV05] which we believe if it can be adopted well, it could increase the reliability and quality of software. This tool also won the APICTA Indonesia award for research and development category. However, to be able to use the tool, not only need training but also require additional basic courses which were not sufficiently provided in our current computer science curriculum.
C. Proposed Learning Activity
We propose a twoone day seminar to disseminate our previous research result funded by the Ministry of Research and Technology. We name the seminar:
A formal method approach for reliable and high quality software
The event will preceded by on-line learning of related basic materials to facilitate thegive participants the gaining foundation and the basic knowledge.
C.1. Rationale
This activity will provide the audiences sufficient motivation to keep improving their software quality by raising some of the issues and the latest findings which they are not aware of before. The activity will provide the audiences which some basic knowledge which is needed to be able to understand the latest approach on improving their software quality.
One example of basic knowledge that IT professionals are lacking is mathematical logic [GS93]. The subject is usually given in the first or second year. However, when they graduate and start working, it is unlikely that they apply it well. As the result, the software is low in quality, the testing become insufficient because the test scenarios are not built based on sufficient logical thinking.
We will provide several discussion sessions for the audiences to simulate how it could be applied. The audiences could freely ask the expert on the related problem they have.
C.2. Objective and Strategy
Our objectives are:
a)Research results dissemination of RUTI-AgI project by faculty of Computer Science UI in collaboration with Utrecht Universiteit[HPA06]. In that research activity we have developed a prototype tool for reliable software engineering. We do not only want to disseminate the prototype and provide some tutorial on how to use it, but we want to provide an advanced knowledge for reliable software engineering which we have learned before especially during the research project. Our previous research result is expected to improve the reliability of the software product which can reduce (or even eliminate) the occurrence of errors (bugs) in software. We expect to improve national competitiveness of software engineering and an efficient investment of ICT through a better quality of software development.
b)We would like to effectively use any possible mean to disseminate our research, in this opportunity, the GDLN network. We believe the use of internet and e-learning module could help us deliver the message throughout the nation and possibly worldwide. This is an effective method to overcome the problem of finding a suitable time and place for both the instructors and the audiences.
c)We expect to meet many potential collaborator and possibly user of our prototype. This opportunity could be use to initiate collaboration which could improve the quality of the research result. This collaboration will strengthen the nation research quality rather than each academician/researcher working alone.
d)We would also like to investigate the possibility to market this new methodology of reliable software development training via e-learning. This is not only reduce the time and cost for the instructor but also to the participant compare to traditional training methods.
C.3. Targeted Audiences
The potential audiences that will benefit and be interested to the proposed learning activity are:
- Computer Science Lecturers. This type of audience needs to keep updating their knowledge with the state of the art. This training provides them with the latest research result which will benefit their students once they graduate and start working as IT professional. It will help the lecturer to prepare well trained graduates.
- Software Engineering Researchers. This type of audience needs to discuss and updating their knowledge. Collaboration among researcher of similar field could improve their productivity.
- Software Engineering Practitioners. We believe that this GDLN and INHERENT network should not only be useful for academician, but it should also be useful for long-life learning by practitioner. Specifically this activity will be the interest of the software engineering practitioner to keep improving their product quality and keep up with the latest state of the art of the practical research result in order to win the IT competition.
- Master students and last year undergraduate students of computer science / information technology study program. This training is not intended for undergraduate student. However, an exception can be made for last year students whose their thesis supervisors also join the seminar or able to guide and help the students in understanding the material. This seminar could give them an overview of the latest trend on software engineering. Some of the prerequisite details which they have not learned or understood should be provided by their supervisors. During or before following this learning activity they should also get additional tutorial from their supervisor.
About 60 – 90 participants are expected in this activity.
There will be four three main stations. We expect 250 participants in GDLN center in Salemba Jakarta , 2015 participants in UNUD Bali, 2015 participants in UIN Riau , 15 participants in UNHAS Makasar and 25 participants spread out using the Inherent network. The participants from Jakarta are expected mostly are practitioners or last year student who are expected to try to apply the knowledge they gain in their daily activity. The discussion session will be prepared to anticipate those needs. While the participants from UIN Riau, UNHAS Makasar and UNUD Bali, are expected to be our future partners in investigating this research area. It is quite difficult to estimate the participants from inherent networks, therefore they will be sufficiently exposed to different aspects during the video conferencing and provided with the complete e-learning material for further studying on their interests.
C.4. Mechanism and Design
This activity is designed in a onetwo days seminar via video conference, preceeded by on-line learning of related basic materials. A week before the seminar, we will provide some multimedia e-learning material contains overview of software engineering process and quality assurance, logic and its role in software engineering and introduction to formal method in software engineering. The material will be uploaded in our Learning Management System called SCeLE. The manual to use the system and the introduction material are given to all registered participants as printed materials to anticipate some participants who are still not familiar with the internet. The participants are also encouraged to start learning and discuss the material via on-line using the forum discussion forum in the SCeLE even before the video conferencing. . Local organizer of each site, is responsible on providing the environment and equipment to do the on-line discussion. Due to limited budget and time, assistants are only provided in the GDLN center (i.e. Salemba, Riau, Makasar dan Bali). The assistants are responsible in helping the participant with the content material especially to help the participant who areparticipants who are not well prepared during the one weekone-week on-line session or need more assistant in understanding the prerequisite knowledge. Both, assistants and local organizer are responsible to provide the required feedback and to initiate the discussion in each site.
It is important to note that relying on the two days video conference period will not be sufficient for the participants even with the sufficient preliminary knowledge to absorb the research result that we want to disseminate. Self studying of the material will also be very difficult and time consuming due to the research nature of the topic which required additional motivation and guidance. The blended learning mechanism is important to effectively deliver the materials. Here, the participants are required to learn the material on-line well before the video conference. During the video conferencing they will be elaborated and guided to the specific aspect of the research result which meets their interest. Therefore the success of this activity is not only depends on the two days video conference but also depend on the participants cooperation during the preceded one week on-line.
In the first day, there will be two sessions. In the first session, our experts will elaborate the subjects and expose all the related aspects which will be the interests of the participants. To prepare the participants, a session of review lecture is given in the afternoon session. After each session, there will be an on-line discussion session for knowledge sharing and question answering with the experts.
To provide prove of concept, the second days will be dedicated for application demonstration and problem solving of a simplified case study. The morning session is the demonstration and the afternoon session is the problem solving exercise of a simplified case study. A slightly different than the first day, in the second day all activity can be interleaved with the on-line discussion activities and most importantly provide interactive environment on the demonstration session. The role of assistants and local organizers are becoming more important in these two sessions. In the problem solving session, the participants are first encouraged to work with a small group and then discuss their solution and finding, with the rest of the participants using the video conference. During their small group discussion, we provide the possibility to contact the available experts. The assistants and local organizer should actively initiate the small group discussion. For those groups who are not ready for group discussion, the on-line discussion forum is still open to let our experts help them preparing themselves and solve their obstacles.
The details activitiyes isare shown in the following table:
Period / Activity / NotesOne week to the seminar / On-line learning and discussion of the basic materials. ThreeFive multimedia e-learning materials are provided:
- Overview of software engineering process and quality assurance
- Logic and its role in software engineering
- Introduction to formal method in software engineering
- FAQ on the above material to answer some of the participant common questions.
- On-line quiz to help the participants evaluate themselves.
SeminarDay 1: session 1 / Video conference (90’)
Topic: Formal method in software engineering
By: Prof. Belawati H Widjaja, Ph.D and L. Y. Stefanus, PhD
Moderator: Siti AminahDina ChahyatiKasiyah, MScKom / Round down of each session of video conference:
5’: ice breaking
5’: informing the topic and the goal
30’: presenting the material
20’: discussion
30’: presenting the material
20’: discussion
10’: wrap up and closing
Day 1: session 2
Seminar: session 2 / Video conference (90’)
Topic: Technology for specifying and generating reliable data processing program
By: Heru Suhartanto, PhD
Moderator: Ade Azurat, SKomKasiyahDina Chahyati, MKomsc,
Day 1: session 3
(discussion) / Local discussion followed by on-line discussion and on-line quiz. (120’)
Moderator:
GDLN Salemba: Dina Chahyati, Mkom, and Kasiyah, Msc
GDLN Riau: Ade Azurat, Skom
GDLN Bali : Siti Aminah, Mkom / The material is provided as mentioned before. This session will be the short version of the one week on-line period.
Round down:
40’: Local discussion
60’: on-line discussion
20’: wrap up and closing
Day 2: session 1 / Video conference (90’)
Topic: Case study
By: Dewi Mairiza, Mkom
Moderator: Rikky Wenang, SKom / Round down:
5’: informing the topic and
the goal
15’: presenting the case
study
20’: discussion
20’: tool demonstration
50’:discussion and
Interactive demonstration
10’: wrap up and closing
Day 2: session 1
(Morning session, parallel with on-line discussion) / Video conference (90’)
Topic: Demo of LinguSQL
By: Rikky Wenang, SKom
Moderator: Dewi Mairiza, Mkom / Round down:
5’: informing the topic and
the goal
15’: presenting the case study
20’: discussion
20’: tool demonstration
50’: discussion and
interactive demonstration
10’: wrap up and closing
Day 2: session 3
(Afternoon session, parallel with on-line discussion) / Problem solving (120’)
Moderator:
GDLN Salemba: Rikky Wenang, Skom and Dewi Mairiza, Mkom
GDLN Riau: Ade Azurat, Skom
GDLN Bali : Siti Aminah, Mkom
GDLN Makasar: Theresia Budiyanti, SKom / Round down:
5’: ice breaking
5’: informing the topic and
case study
40’: small group discussion
40’: selected group
presentation
40’: local group discussion
90’: online-discussion
15’: expert/moderator
comments and wrap up
5’: closing
C.5. Institutional Arrangement
These activities will be based in Faculty of Computer Science, University of Indonesia. All the speakers are from Fasilkom UI, who also the member of the previous research. Dr. I.S.W.B Prasetya from Utrecht Universiteit, our partner in the research, will be one of the subject matter experts especially in material development process.