\section{Introduction} \label{sec:intro}
The utility of formal methods in the development of high assurance systems has gained widespread use in some segments of industry. With the use of formal methods, there are two main approaches for providing assurance. The first approach, {\em correct-by verification}, is the most commonly used approach. In this approach, one begins with an existing model (or program) and a set of properties (specification), and verifies that the given program meets the given properties of interest. An embodiment of this approach is {\em model-checking} \cite{bcmdh92, spin, slam, lpy97} and has been widely studied in the literature. However, a pitfall of this approach is that if the manually designed model does not satisfy the requirements then it is often unclear how one can proceed further. Hence, for scenarios where an existing model needs to be revised to deal with the new environment, the new identified faults, or the new requirements, one needs to manually develop the new model if one needs to obtain assurance via modeling checking.
The second approach, {\em correct-by-construction}, utilizes the specification of the desired system and constructs a model that is correct. Examples of this approach include \cite{ec82, mnp06, afh96, aae98,ae01, kv01}. These approaches differ in terms of the expressiveness of the specifications they permit and in terms of their complexity. However, a pitfall of this approach is the loss of reuse (of the original model) and a potential for significant increase in complexity.
To obtain the benefits of these two approaches while minimizing their pitfalls, one can focus on an intermediate approach, {\em model revision}. Model revision deals with the problem where one is given a model/program and a property. And, the goal is to revise the model such that the given property is satisfied. Applications of model revision include scenarios where model checking concludes that the given property is not satisfied. Other applications include scenarios where an existing model needs to be revised due to changes in requirements and/or changes in the environment. For this reason, model revision has been studied in contexts where an existing model needs to be revised to add new fault-tolerance properties, safety properties, liveness properties and timing constraints \cite{borzoothesis}.
Since model revision results in a model that is correct-by-construction, it provides assurance comparable to {\em
correct-by-construction} approaches. Also, since it begins with an existing model, it has the potential to provide reuse during the revision process. Moreover, there are several instances where complexity of model revision is comparable to that of model checking \cite{borzoothesis}.
Based on these observations, our goal in this paper is to illustrate the application of model revision in the context of a case study from automotive systems. One problem in applying formal methods in industrial systems is the high learning curve encountered in formal methods. One approach to reduce the learning curve is to utilize an existing framework utilized by designers and allow formal methods to be hidden under the hood.
One challenge of exploring such an approach of applying the model revision is that the current model-based design is often modeled in a noncomputatonal way, such as UML. UML \cite{UML2004} is a well-known modeling language utilized by industry, with focus on system architecture as a means to organize computation, communication and constraints. Of UML diagram sets, State diagram is especially helpful when designers discuss the logic architecture and workflow of the whole system with the need of independence from a particular programming language. Since the UML state diagram is able to illustrate the high-level overview of the whole system, it is widely used to model program design. With this motivation, the approach in our paper starts with program design modeled in the UML state diagram.
To overcome the challenge of applying model revision on program design modeled in UML state diagram, that is, model in UML state diagram is not computational one, our approach proposes an automatic transformation mechanism from model in UML state diagram to the underlying computational model. Subsequently, the model revision algorithms are applied on the program modeled in the corresponding underlying computational model. Finally, the revised program modeled in the underlying computational way is converted into program design modeled in UML state diagram with fault-tolerance properties. We illustrate the whole work-flow with a case study from automotive systems- the adaptive cruise control system.
{\bf Organization of the paper. } The rest of the paper is organized as follows. In Section \ref {sec:moti}, we illustrate the proposed approach by presenting a motivating scenario from design issues in automotive system. In Section \ref{sec:modeling}, we briefly discuss the related concepts of modeling program design and introduce the underlying computational model. Next, in Section \ref{sec:framework}, we describe the work-flow of the proposed framework step by step. Related work is discussed in Section \ref{related}. Finally Section \ref {sec:Conclusion} makes concluding remarks.
\iffalse
\section{Introduction}
Modern industry critical systems often face challenge caused by uncertainties in deployment environment. Uncertainties in industry critical systems design keep increasing for two reasons \cite{Henzinger06theembedded}: 1) the deployment environments are not easy to perfectly predicated since systems are deployed in a greater variety of situations, and 2) systems are implemented on sophisticated, hardware/software layered multicore architectures with cashes, pipelines and speculative executions due to the rapid of progress in VLSI design.
Due to the economic and practical issues, it is impossible to design a system from start to satisfy the requirement of every specific environment. Hence, a natural task for designer of industry critical system is how to revise the existing system design to satisfy the new specification. Moreover, when revising the current design to satisfy new specification, how is the revised design guaranteed to keeps the existing specification? These questions motivate us to explore an approach to assist the system designer to revise program design in an automatic and guaranteed-correctness manner.
One challenge of exploring such an automatic approach is the current model-based design is modeled in a noncomputatonal way, such as UML and AADL. UML \cite{UML2004} is a well-known modeling language with focus on system architecture as a means to organize computation, communication and constraints. Of UML diagram sets, State diagram is especially helpful when designers are discussing the logic architecture and workflow of the whole system with the need of independence from a particular programming language. Since the UML state diagram is able to illustrate the high-level overview of the whole system, the approach in our paper use UML state diagram to model system design.
Considering model revision technology has been proved to be a feasible approach to automatically synthesize new specification to the existing program, our framework utilize this technology to revise the program design modeled in the underlying computational model. Towards applying the model revision technology, our framework proposes the mechanism to transform the model in UML state diagram to the underlying computational model accepted by the model revision engine. Such automatic transformation mechanism overcomes the weakness of model-based design (in UML state diagram), that is, current model-based design is not in computational model. In our paper, we demonstrate the whole workflow of the proposed framework by a motivating scenario in cyber physical system- an adaptive cruise control system.
\fi