The 2nd GRACE Seminar on Software Science and Engineering

Date: 4 June, 2008 (Wed)
Time: 10:00-12:00
Place: Seminar Room 1 (2006) on 20F, NII
Fee: Free
Contact: Zhenjiang Hu (hu _AT_ nii.ac.jp)

Program
1. Correct Functional Parallel Programs in a Safe Execution Environment
Frederic Loulergue (LIFO, University of Orleans)

Abstract:The design of parallel programs and parallel programming languages is a trade-off. On one hand the programs should be efficient. But the efficiency should not come at the price of non portability and unpredictability of performances. The portability of code is needed to allow code reuse on a wide variety of architectures and to allow the existence of legacy code. The predictability of performances is needed to guarantee that the efficiency will always be achieved on any architecture.

Another very important characteristic of parallel programs is the complexity of their semantics. Deadlocks and indeterminism often hinder the practical use of parallelism by a large number of users. To avoid these undesirable properties, a trade-off has to be made between the expressiveness of the language and its structure which could decrease the expressiveness.

Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism: deadlocks are avoided and indeterminism is limited to very specific cases in the BSPlib. BSP programs are portable across many parallel architectures.

The Bulk Synchronous Parallel ML language (BSML) is based on a confluent extension of the λ-calculus. Thus it is deadlock free and deterministic. Being a high-level language, programs are easier to write, to reuse and to compose. It is even possible to certify the correctness of BSML programs with the help of the Coq proof assistant. However the correctness of these programs is ensured with respect to the programming model of BSML. BSML, as data-parallel languages, has a programming model that is a formal or informal semantics of the primitive operations it provides as viewed by the programmer. However the realization of the primitives on parallel architecture, or execution model, is quite different. Thus to guarantee the correct execution of these programs in parallel, it is necessary to verify the equivalence of the programming model and the execution model.

This talk presents the Bulk Synchronous Parallel language, several formal semantics of BSML from the programming model to the semantics of an abstract parallel machine, and proof of correctness of BSML programs with the Coq proof assistant.

2. Formal Engineering Methods for Software Quality Assurance
Shaoying Liu (Department of Computer Science, Hosei University)

Abstract: Conventional software engineering based on informal or semi-formal methods are facing tremendous challenges in ensuring software quality. Formal methods have attempted to address those challenges by introducing mathematical notation and calculus to support formal specification, refinement, and verification in software development. However, in spite of their theoretical potential in improving the controllability of software process and reliability, formal methods are difficult to apply to large-scale and complex systems in practice due to many constraints (e.g., limited expertise, complexity, changing requirements).

We have developed the “Formal Engineering Methods” (FEM) as a research area since 1990 to study how formal methods can be effectively integrated into conventional software engineering process so that formal techniques can be tailored, revised, or extended to fit the need for improving software productivity and quality in practice (e.g., through the enhancement of the usability of formalism and the tool supportability of the relevant methods). We have also developed a specific FEM called Structured Object-Oriented Formal Language (SOFL) that offers three rigorous but practical techniques for system modeling and verification: three-step formal specification, specification-based inspection, and specification-based testing. The effective combination of these three techniques can significantly enhance software productivity and quality. The SOFL method has also achieved a good balance among simplicity, visualization, and preciseness to allow engineers to easily use the method. In this talk, I will focus on the discussion on the issue of how FEM is used for software quality assurance.

This entry was posted in Research, Seminar. Bookmark the permalink.

Comments are closed.