In addition to software development techniques such as formal methods, software process is important for effectively developing quality software. In the literature, we have well-defined process templates which provide mechanisms for measuring, controlling, managing, and improving the way we develop software. Well-defined process templates can serve as a vehicle to integrate advanced software engineering techniques, such as formal methods, into actual software development. We expect that students who have mastered such a well-defined process template can effectively use formal methods and understand the effectiveness of formal methods. In this paper, we report on a trial case of team software process in which students tried using a model-oriented formal specification language in a lightweight way for their project. We generated a hypothesis that students with some process capabilities understand the effectiveness of rigorously writing specifications in a formal specification language while students with less capabilities do not.
Formal methods are useful to effectively develop quality software. However, students who have been taught formal methods seem to seldom use them in their actual software development process. We need methods to convince students of the effectiveness of formal methods in their actual software development.
In addition to formal methods, software process is important in order to effectively
develop quality software. For example, there is a claim “effective processes provide a
vehicle for introducing and using new technology in a way that best meets the
objectives” in a document of process improvement framework [
Our current focus is the combination of a model-oriented formal method we can use
in a lightweight way and a well-defined customizable process template supported by a
process improvement framework [
In this paper, we report lessons learned from a trial case of team software process in which students tried using a model-oriented formal specification language in a lightweight way for their project. As we have not collected strong evidence as in controlled experiments, we discuss our trial descriptively here. In Section 2, we explain our approach of integrating formal methods into well-defined software processes. In Section 3, we explain PSP and our trial of the combination of VDM and PSP. In Section 4, we explain TSP and our trial of the combination of VDM and the introductory TSP, before concluding in Section 5. 2
2.1
We use TSP and PSP, developed and managed by CMU (Carnegie Mellon
University) SEI (Software Engineering Institute), as our baseline process templates. These
are widely known as scalable, measurable and customizable processes [
There are various ways of using formal methods in design flows. In this paper, we use
a light weight approach in which the rigor level of the design flow is Level 3 or 4
according to the seven levels of increasing rigor of design flows proposed in [
Level 2: Conventional design flow, with semi-formal specifications.
Level 3: Formal design flow, with formal specifications and without tool support. This is basically a conventional design flow in which formal specifications replace informal/semiformal ones. Most of quality control and quality assurance remain achieved using conventional quality steps. Level 4: Formal design flow, with formal specifications and lightweight checking tools.
The specifications are written in formal languages equipped with syntax and static semantics checkers, which can detect shallow mistakes (e.g., syntax errors, undeclared identifiers, type inconsistencies, etc.).
Level 5: Formal design flow, with formal specifications and bug hunting tools. Level 6: Formal design flow, with formal specifications and proof tools.
Level 7: Formal design flow, with formal specifications, proofs, and proof checking tools.
There are no direct relationships between this rigor level and the levels in CMMI, capability level and maturity level. However, we can use formal methods for the important process elements such work-products and practices in process improvement.
We basically recommend a lightweight approach when starting to use formal methods. In a lightweight approach, we develop a formal specification and then work-products int the next level from the specification informally. Lightweight approaches to formal methods seem cost effective and likely to be adopted in a wider range of actual development, while the specific level of rigor depends on the goal of the project. In lightweight formal methods, we do not rely on very rigorous means, such as theorem proofs. Instead, we use adequately less rigorous means, such as writing specification in a formal specification, evaluating pre/post conditions and testing the specification, to increase our confidence in the specification. 3 3.1
We briefly introduce PSP without going into the details, as the details of PSP can be
found in the literature [
As shown in Fig. 2, PSP0 and PSP1 consist of the following phases: planning, detailed design, code, compile, test, and postmortem. PSP2 has extra two review phases: planning, detailed design, design review, code, code review, compile, test, and postmortem. In PSP2, four specification templates are provided: operational, functional, state and logic specification templates. Developers can improve quality of their products by using these specification templates and reviewing them with a review checklist in PSP2. Fig. 3 shows scripts of Detailed Design and Design Review phases in PSP2. Developers can measure and analyze the effectiveness of these templates and activities related to these templates through the measurement and analysis mechanism in PSP.
Once developers have established their development process as in PSP2, we expect
they are ready to introduce formal methods in their process improvement. PSP was
developed based on the CMM (CMMI’s predecessor), and designed to be CMM level
5. PSP has a process improvement mechanism as in CMM. In the continuous
representation of CMMI, the set of process areas for level 2 includes MA, Measurement
and Analysis process area. For example, we can focus on the defect types which are
frequently injected and expensive to fix according to the process data once we have
established such practices in PSP that reflects MA in CMMI. In addition, we can
customize the baseline process template to include the work-products and activities with
formal methods effective in preventing injection of defects of the specific defect types
[
The four specification templates in PSP can be replaced with those written in
formal specification languages. One instance is an approach with a model-oriented
formal method VDM, one of the longest-established formal methods for the
development of computer-based systems. By using VDM, we can enhance and improve the
work-products and activities in Detailed Design and Design Review phases. We can
use the standard language the VDM Specification Language (VDM-SL) and dialects
such as VDM++, which supports the modeling of object-oriented and concurrent
systems. There exist textbooks corresponding to these languages such as [
In our trial using VDM in a personal process [
After considering the lessons learned from our trial on PSP mentioned above, we
continue to extend our trial to a team-level software development process, TSPi (Team
Software Process introduction) [
Each cycle is divided into eight phases, launch/re-launch, strategy development, planning, requirements, design, implementation, testing, and postmortem phase. TSPi is a defined and customizable team process, and has scripts that cover issues such as what kind of work to be done in each phase and how to collect process data. As TSPi is
Fig. 3. Scripts of Detailed Design and Design Review Phases in PSP2 a defined process that can be tailored, we can integrate formal methods with TSPi, and evaluate the effectiveness using its process data. 4.2
In this case, we focus on problems related to design activities among team members. In TSPi, one or two members develop a high-level design, and each member is assigned his/her task based on the high-level design. Each member develops the detailed design for his/her task before proceeding to the coding task in the coding phase. In our trial, we compare the defect data when using the normal TPSi design flow with those when we enhance the design flow with VDM in order to observe the effectiveness of using VDM.
In this case, the team used VDM as follows. 1. The team members follow the standard script and templates for the design phase in
TSPi. 2. The team members complete reviews and inspections. 3. The team members collect and the record the defect data for the design phase. 4. The team members redo the design using VDM. 5. The team members use VDMTools for syntax and type checking of their design. In addition, they use the tool for animating the selected part of the design. 6. The team members collect and the record the defect data additionally found by using VDM.
Among the defects, we picked up the defects related to interface, data type, and functionality in the discussion below. This means we exclude the minor defects like typing errors. During the standard TSPi design flows, they found 2 defects in the highlevel design and 37 defects in the detailed design. By using VDM, they additionally found 23 defects. These were the defects of the high-level design itself and the defects of the detailed design caused due to the flaw in the high-level design. While the members might not be practiced in reviewing and inspecting, they missed defects in the design of the normal design flow using non-formal and semi-formal notations.
Ideally, members of TSPi are expected to be practiced with their personal software process capabilities. Students are required to follow the monitoring practices like specific practices in Measurement and Analysis process area in CMMI-DEV throughout the PSP course. They also need to submit reports that require capabilities like those in Causal Analysis and Resolution process area. In our TSPi trial, members were not equally practiced with their personal software process capabilities. A few of them were practiced and the rest of them were not. According to our impression from interviews with the members, more practiced team members seemed to understand the effectiveness of formal methods more concretely while less practiced member seemed to feel more vaguely. We generated a hypothesis that students with higher process capabilities understand effectiveness of rigorously writing specifications in a formal specification language while students with lower capabilities do not. We have been working on the effective methodology of introducing formal methods into the actual software development process. We reported our trial case of software process in which students tried using a model-oriented formal method in a lightweight way for their project. We only have very limited data so far. However, we generated a hypothesis from our trial case that students with some process capabilities can better understand the effectiveness of rigorously writing specifications using formal method while students with less capabilities do not. We will continue and extend our effort to collect evidence to support our hypothesis.