Keynote Speech at ICFEM 2012, Kyoto

Toward Practical Application of Formal Methods
in Software Lifecycle Processes

November 14, 2012

Mario Tokoro
Research Supervisor, JST/CREST DEOS ProjectSony Computer Science Laboratories, Inc.

Background• Large Information Systems are continuously used for a long period of time,
while constantly being modified due to unexpected changes in, e.g.,– Service Objectives– Users’ Requirements– Evolving Technologies– Regulations and Standards• These systems include externally-developed modules, and are often
connected to external systems, and might run on unknown environments(clouds)• The development and modification of a system is performed concurrently
with the system’s operation, and it is almost impossible to view the life of
the system as a temporal and spatial concatenation of static and isolatedsystems.
• Existing software lifecycle processes can hardly cope with these situations,whereas, achieving dependability in such an ever-changing system has
become one of the most demanding system issues to be solved.
November 14, 2012

©Mario Tokoro

2

Background• Large Information Systems are continuously used for a long period of time,
while constantly being modified due to unexpected changes in, e.g.,– Service Objectives– Users’ Requirements– Evolving Technologies– Regulations and Standards• These systems include externally-developed modules, and are often
connected to external systems, and might run on unknown environments(clouds)• The development and modification of a system is performed concurrently
with the system’s operation, and it is almost impossible to view the life of
the system as a temporal and spatial concatenation of static and isolatedsystems.
• Existing software lifecycle processes can hardly cope with these situations,whereas, achieving dependability in such an ever-changing system has
become one of the most demanding system issues to be solved.
November 14, 2012

©Mario Tokoro

3Consistency throughout Lifecycleis hard to be kept
Specification

Implementation

Aim

Output$#!

*$&*#%!

Changing Environments• Service objectives• Users’ requirements• Available technologies• Standards• Regulations, etc…

November 14, 2012

©Mario Tokoro

Indeterminacy Problem

4Our Approach• An approach to ever-changing systems– the boundary– Functions– structures– interfaces• We need to consider the Indeterminacy Problem• Thus, we need to give up completeness• We view such system as Open Systems (thanClosed systems).
November 14, 2012

©Mario Tokoro

5

Closed Systems vs. Open Systems
Closed Systems

Open Systems
Subsystem

Subsystem

Subsystem
Subsystem

Subsystem

Subsystem

Subsystem

Subsystem
Subsystem

Subsystem

Subsystem
Subsystem• The boundary of the system is definable.
• Interaction with the outer world is limited,
and the system functions are fixed.
• The subsystems or components of the system
are fixed and their relationship does notchange over time.
November 14, 2012

• The boundary of the system changes over time.
• Interaction with the outer world and the system
functions change over time.
• The subsystems or components of the systemand their relationship change over time.

©Mario Tokoro

6

Open Systems Dependability• A system whose function, structure and boundary keep changing
over time is called an open system in contrast to a closed system
whose function, structure, and boundary stay the same through thelife of the system.
• We define Open Systems Dependability as the property of a systemsuch that it has the ability– to continuously remove problem factors which may cause
failures,– to take a quick and appropriate action when a failure occurs tominimize damage,– to safely and continuously provide the services expected byusers as much as possible, and– to maintain accountability for the system operations andprocesses.
November 14, 2012

©Mario Tokoro

7

DEOS Process• DEOS process implements Open Systems Dependability• DEOS process treats the initial development, themodification of a system, and system operation as anintegrated iterative lifecycle process.
• It includes
1.
2.

3.
4.

Change Accommodation Cycle to accommodate requirementchanges in service objectives and environments
Failure Response Cycle to respond quickly and properly tofailures
D-Case, which is an extension of Assurance Cases, forstakeholders to achieve consensus on dependability issues,andThe DEOS architecture which provides a database called DADD to retain D-Cases and an application-oriented runtime
environment for flexible monitoring and control functions.

November 14, 2012

©Mario Tokoro

8The DEOS Process Iterative process• Change Accommodation Cycle to accommodate requirement changes inservice objectives and environments• Failure Response Cycle to respond quickly and properly to failures
 Agreement Description Database (D-ADD) including D-Case plays the key rolesof consensus building and of integration of development and operation phases

November 14, 2012

©Mario Tokoro9

Achieving Stakeholders’ Agreement andAccountability through D-Case••••••

D-Case is an argumentation method/tool
extended from assurance cases to be used inthe development and operation phases
We use the structural notation called GSN(Goal Structuring Notation) with Goal,
Strategy, Context, Evidence, andUndeveloped Nodes
We added Monitor Node to glue thedevelopment and operation phases
We added External Node to incorporate
externally developed modules and to use
external services
Description in Natural Language, Pseudo(Controlled) Natural Language such as SBVR,
or more formal way in Agda
Will be used to determine the level ofdependability (like SIL or ASIL)

November 14, 2012

©Mario Tokoro

10

Coping with Externally-Developed Modules
and Connection to External Systems•••

Off-the-shelf modules
Legacy codes
External services throughnetworks• Systems may run in unknown
environment such as clouds•System BSystem ABAd（B) to assurethat B isdependable

D-Case Reverse Engineering inaddition to Forward Engineering

November 14, 2012

©Mario Tokorod（A) to assurethat A is
dependabled（A,B) assuresthat B meets A’sdependability
requirementsd（A,C) assures thatsubsystem C meetsA’s dependability
requirements

Cd（C) to assurethat C isdependable

System C11

DEOS Architecture
A DEOS architecture supports the execution of the DEOS process Agreement Description Database (D-ADD) which retains all the D-Case descriptions, Tools to support requirements management, Tools to develop dependable software (D-DST) Execution Environment to execute programs, to monitor and record the states ofprograms, and to respond to failures (D-RE)

November 14, 2012

©Mario Tokoro12

Binding Development and Operation Phases•••

Monitor Node in D-Case designates
monitoring the operation and logging
data
D-Script describes responsive actions
to be taken when operation shows asign of failure or when operation fails
D-Script Engine is designed to provide
flexible yet secure man-machineinterface in execution of D-Script•D-ADD retains all the D-Casedescriptions historically with thereasons why such decisions have beenmadeD-ADD contributes, when a system is tobe modified, to achieve stakeholders’agreement
D-ADD contributes, when a system fails,
to analyze causes of failures••

Programs

D-Application Manager
D-CaseD-Script
Agreement
Description
Database
November 14, 2012

D-Box
Linux

D-Script D-Script
EngineD-SystemMonitorD-Application
MonitorOS

D-Visor©Mario Tokoro

Hardware/TCB

13

D-ADD Consists of 3 Layers•••

Fundamental Tools Layer which provide user interface tools
Model Layer which associates agreement graph with D-Cases and evidences
including documents and logged data
Repository Layer which provides the storage

Monitoring
Support of Consensus Building
Contract Development

Fundamental Tools Layer

D-CaseMeeting
ToulminConsensus Building･･･
Organization Fundamental Data

Models Layer

Repository Layer

Graph DB
November 14, 2012

Key/Value Store
Document DB©Mario Tokoro

14How can we apply Formal Methods
in Software Lifecycle Processes
for Open Systems?

November 14, 2012

©Mario Tokoro

15

Formal D-Case for Rigorous V&V (1)• Verification and Validation (Barry Boehm):– Verification :Are we building the system right?

w.r.t. given, specified criteria: spec, operational conditions, …

– Validation:

Are we building the right system?

w.r.t. “Real World” : user needs, actual environment, …

• Our thesis on D-Case:
A formal D-Case ≈ ⟨ a formal theory , a formal proof in it ⟩Cf. Y. Kinoshita and M. Takeyama, keynote speech to be given in Safetycritical Software Symposium 2013.

– Formal theory codifies the agreed vocabulary and reasoning principles
about the system, environment and processes.
– Formal proof represents the verification argumentof the agreed formal claim that specifies what is “right”
Proof assistants, such as Agda, support its construction/checking
November 14, 2012

©Mario Tokoro16

Formal D-Case for Rigorous V&V (2)• Rigor in V&V enabled by formal D-Case:
Rigor in Verification: Communication through a formal DCase
Rigor in Validation: Requirements for a formal D-Case
Requirements for a positive answer to “Are we verifying thesystem right w.r.t. the current best practice?”• But beware! We can never say we built a 100% right system.
∵ its rightness is w.r.t. the real world.
Validation is inherently a vaguely defined action that ideally is neverending (open systems viewpoint).

• Yet we can say something definite about theconformance to the requirements of best practices.
Proof assistants, such as Agda, help here, too.
November 14, 2012

©Mario Tokoro

17

D-Case/Agda (“D-Case in Agda” Verification Tool)
supports checking/construction of formal D-Cases
Checking, construction, generation of D-Cases
as formal proofs using Agda proof assistantNovember 14, 2012

©Mario Tokoro

Graphical edit,
domain-expert review
using D-Case Editor

18

Applying Formal Methods to Open Systems
Specification

Implementation

AimOutput$#!

*$&*#%!

VerificationValidation

Repetitive Application of Formal D-Case to an open system forMore Rigorous in Verification and in Validation
User Interfaces for Formal Methods are getting more important
November 14, 2012

©Mario Tokoro

19About the DEOS Project
Dependability Engineering for Open Systems••••

A project under Japan Science and Technology Agency (JST)Roughly $60M in total over 7.5 years started in 2006
5 teams selected in 2006 and 4 teams in 200817 professors, 8 researchers from national laboratories, morethan 40 post-docs, and many graduate students have workedtogether.
• R&D Center (DEOSC) was established in 2007 for supporting
development, integrating codes developed by the teams, andpromoting the use.
November 14, 2012

©Mario Tokoro

20Current Status• The DEOS process is defined• Prototype Architectures have been
demonstrated• D-Cases are described for a few
systems and more
• A book is published from CRC
Press in October• Other books are being written,e.g., on D-Case, D-ADD, D-Script…
• We are promoting international
standardization (see next pages).
November 14, 2012

©Mario Tokoro

21

Standardization (1)Purpose Sharing the concepts of Open Systems Dependability
 Provide guidelines for IT systems for social infrastructures
 Achieving common use of tools

We have been active in IEC and ISO standardization efforts
 IEC TC56 (Dependability)• The concept of Open Systems Dependability was submitted as
NWIP to IEC TC56 in September 2012
• Participating as experts: IEC60300-1(Dependability management),
IEC62741(Dependability case), andIEC62628(Guidance on software aspects of dependability) ISO/IEC JTC1/SC7 (Software and systems engineering)• Standards for methodology of consensus building, achieving
accountability and process• ISO/IEC15026 Systems and Software Assurance (Co-editor)
November 14, 2012

©Mario Tokoro22

Standardization (2)Purpose To contribute to Users

We have been working with The Open Group: To contribute to TOGAF 9.1 and/or TOGAF Next Generation wrt
Dependability Importance of Change Management (the notion of Open Systems
Dependability) for achieving Dependability Necessity of Integrating Development and Operation into a single
iterative process (the DEOS Process) Importance of Stakeholders’ Agreement and Accountability
Achievement through an assurance case (D-Case with RTES“Dependability Through Assuredness” ) and its history
 D-Case Tools, D-ADD Implementations, etc.
November 14, 2012

©Mario Tokoro23

We much appreciate your support and participation.
For more information, please send e-mail tomario.tokoro@csl.sony.co.jp

Thank you
JST/DEOS Center
http://www.dependable-os.net/index-e.html
JST/DEOS Project
http://www.jst.go.jp/kisoken/crest/en/category/area04-4.html
Sony Computer Science Laboratories, Inc.
http://www.sonycsl.co.jp
November 14, 2012

©Mario Tokoro

24