Final Disccsion with idir Nico

src/ontologies/ARINC661/ARINC_661.thy

@@ -0,0 +1,240 @@
+theory ARINC_661
+  imports  "Isabelle_DOF.technical_report"
+
+begin
+
+(* COCKPIT DISPLAY SYSTEM = CDS *)
+
+datatype A661_BOOL = 
+                    A661_TRUE
+                  | A661_FALSE
+                  | A661_TRUE_WITH_VALIDATION 
+
+datatype Alignment = 
+                     A661_BOTTOM_CENTER 
+                   | A661_BOTTOM_LEFT 
+                   | A661_BOTTOM_RIGHT 
+                   | A661_CENTER 
+                   | A661_LEFT
+                   | A661_RIGHT 
+                   | A661_TOP_CENTER 
+                   | A661_TOP_LEFT 
+                   | A661_TOP_RIGHT
+
+datatype WidgetType = 
+                  (* Containers *) 
+                    A661_PANEL        
+                  | A661_BASIC_CONTAINER 
+                  | A661_BLINKING_CONTAINER
+                  | MutuallyExclusiveContainer 
+                  | TranslationContainer 
+                  | RotationContainer 
+                  | BlinkingContainer 
+                  | TabbedPanelGroup 
+                  | TabbedPanel 
+                  | ScrollPanel 
+                  (* Graphic widgets  *)
+                  | A661_ACTIVE_AREA
+                  | A661_LABEL 
+                  | LabelComplex
+                  (* Interactive widgets *)
+                  | PushButton 
+                  | ToggleButton 
+                  | EditBoxNumeric 
+                  | CheckButton 
+                  | ComboBox 
+                  (* Map widgets *)
+                  | MapHorz
+                  (* Utility widgets *)
+                  | Connector
+                  | A661_PICTURE
+                  | A661_SYMBOL
+                  | A661_PICTURE_PUSH_BUTTON
+
+doc_class Widget =
+          name  :: string
+          widget_type  :: WidgetType
+          widget_ident :: int
+          parent_ident :: "int option"
+
+doc_class Layer =
+          name            :: string
+          layer_id        :: int
+          context_number  :: int
+          height          :: int
+          width           :: int
+          visible         :: bool
+          enable          :: A661_BOOL
+          widgets_tree    :: "Widget set"
+
+(* invariant : When a layer becomes inactive, its visibility is turned off 
+by the CDS (an exception to this is when a NoServiceMonitor widget is present in the layer; *)
+
+doc_class Window =
+          application_id   :: int
+          height           :: int
+          width            :: int
+          be_resized       :: bool <= True
+          contained_layers :: "Layer set"
+          type_synonym DefinitionFile = Window
+          type_synonym DF = DefinitionFile
+
+doc_class DisplayUnit = 
+          contained_windows :: "Window set"
+          type_synonym DU = DisplayUnit
+          type_synonym UserApplication = DisplayUnit
+          type_synonym UA = UserApplication
+
+doc_class CockpitDisplaySystem =
+          name             :: string
+          contained_du     :: DisplayUnit
+          type_synonym CDS = CockpitDisplaySystem
+
+section\<open>WIDGET LIBRARY\<close>
+
+text\<open>The ActiveArea is transparent rectangular widget. 
+The ActiveArea may have a graphical representation when this widget is highlighted 
+or when it has the focus. A selection of this widget by a crew member initiates 
+an event notification sent to the owner UA of the widget. \<close>
+
+doc_class ActiveArea = Widget +
+          widget_type           :: WidgetType <= A661_ACTIVE_AREA
+          visible               :: bool
+          enable                :: A661_BOOL
+          (* style_set :: ? *)
+          pos_x                 :: int
+          pos_y                 :: int
+          size_x                :: int
+          size_y                :: int
+          next_focused_widget   :: int
+          (* automatic_focus_motion :: ? Automatic motion of the focus on widget specified in NextFocusedWidget parameter *)
+          EntryValidation       :: bool
+          (* Indicator notifying the CDS that the UA has completed processing the entry or selection event. This flag also indicates the results of that processing *)
+          invariant force_widget_type_1 :: "widget_type \<sigma> = A661_ACTIVE_AREA"
+
+text\<open>The BasicContainer has no graphical representation. Its purpose is to group children widgets 
+and to provide a means for managing the visibility and the interactivity of this set of widgets. 
+The contained widgets are positioned with respect to the PosX, PosY of the BasicContainer. 
+The position of the BasicContainer can be changed at run-time.\<close>
+
+doc_class BasicContainer = Widget +
+          widget_type           :: WidgetType <= A661_BASIC_CONTAINER
+          visible               :: bool
+          enable                :: A661_BOOL
+          pos_x                 :: int
+          pos_y                 :: int
+          invariant force_widget_type_2 :: "widget_type \<sigma> = A661_BASIC_CONTAINER"
+
+text\<open>A BlinkingContainer is intended to apply blinking behavior to a group of widgets.\<close>
+
+doc_class BlinkingContainer  = Widget +
+          widget_type           :: WidgetType <= A661_BLINKING_CONTAINER
+          visible               :: bool
+          blinking_type         :: int (* Type of blinking (appearance to be defined by the aircraft OEM). Value of zero means no blinking. The definition of all other 255 values is determined by OEM. *)
+          invariant force_widget_type_3 :: "widget_type \<sigma> = A661_BLINKING_CONTAINER"
+
+text\<open>A Panel widget groups several widgets together in a rectangular area with clipping capabilities. 
+Widgets placed within a Panel widget have their coordinates referenced to the PosX, PosY 
+reference point of the Panel.\<close>
+
+doc_class Panel = Widget +
+          widget_type           :: WidgetType <= A661_PANEL
+          visible               :: bool
+          enable                :: A661_BOOL
+          (* style_set :: ? *)
+          pos_x                 :: int
+          pos_y                 :: int
+          size_x                :: int
+          size_y                :: int
+          (* TO BE COMPLETED *)
+          (* ADDED PROP *)
+          contained_widgets     :: "Widget set"
+          invariant force_widget_type_5 :: "widget_type \<sigma> = A661_PANEL"
+          
+text\<open>A Label widget consists of a text field at a defined display location. If the label is anonymous, 
+it cannot be modified at runtime by the UA. If it is not anonymous, it can be modified by the UA\<close>
+
+doc_class Label = Widget +
+          widget_type           :: WidgetType <= A661_LABEL
+          visible               :: bool
+          anonymous             :: bool
+          (* style_set :: ? *)
+          pos_x                 :: int
+          pos_y                 :: int
+          size_x                :: int
+          size_y                :: int
+          label_string          :: string
+          max_string_length     :: int
+          alignement            :: Alignment
+          (* TO BE COMPLETED *)
+          invariant force_widget_type_4 :: "widget_type \<sigma> = A661_LABEL"
+
+
+text\<open>A Picture widget is a reference to an image available in the CDS. 
+The Picture reference can be modified by the UA\<close>
+
+doc_class Picture = Widget +
+          widget_type           :: WidgetType <= A661_PICTURE
+          visible               :: bool
+          anonymous             :: bool
+          (* style_set :: ? *)
+          pos_x                 :: int
+          pos_y                 :: int
+          size_x                :: int
+          size_y                :: int
+          (* picture_reference :: ? *)
+          (* TO BE COMPLETED *)
+          invariant force_widget_type_6 :: "widget_type \<sigma> = A661_PICTURE"
+
+text\<open>The Symbol widget is similar to the Label widget, except it does not have a Max-String-Length 
+parameter and the string parameter is replaced by a Symbol- Reference parameter (outside reference).\<close>
+
+doc_class Symbol = Widget +
+          widget_type           :: WidgetType <= A661_SYMBOL
+          visible               :: bool
+          anonymous             :: bool
+          (* style_set :: ? *)
+          pos_x                 :: int
+          pos_y                 :: int
+          (* TO BE COMPLETED *)
+          invariant force_widget_type_7 :: "widget_type \<sigma> = A661_SYMBOL"
+
+text\<open>A PicturePushButton widget is a PushButton including a picture and possibly a string.\<close>
+
+doc_class PicturePushButton = Widget +
+          widget_type           :: WidgetType <= A661_PICTURE_PUSH_BUTTON
+          visible               :: bool
+          enable                :: A661_BOOL
+          anonymous             :: bool
+          (* style_set :: ? *)
+          pos_x                 :: int
+          pos_y                 :: int
+          size_x                :: int
+          size_y                :: int
+          (* picture_reference :: ? *)
+          (* TO BE COMPLETED *)
+          invariant force_widget_type_8 :: "widget_type \<sigma> = A661_PICTURE_PUSH_BUTTON"
+
+
+section\<open>UA Validation\<close>
+text\<open>
+After the "@{typ \<open>CDS\<close>}"  sends a pilot interaction event to the "@{typ \<open>UA\<close>}", 
+the "@{typ \<open>CDS\<close>}" may suspend further pilot 
+interactions (exact scope is implementation dependent) to allow the  "@{typ \<open>UA\<close>}" 
+time to validate the event. In order for this to occur, all of the following are required:
+
+1 - CDS will need to know which specific widget instances contain events which will need to be 
+validated by the UA. To support this the "@{typ \<open>UA\<close>}" ("@{doc_class DisplayUnit}")  
+ must set the Enable (A661_ENABLE) parameter 
+to A661_TRUE_WITH_VALIDATION for each applicable widget instance in either the DF and/or 
+during run-time.
+
+2 - The UA will need to send a notification to let the CDS know when the UA has completed 
+validating the event. This is accomplished when the UA sends the Run-time Modifiable 
+Parameter A661_ENTRY_VALID.
+
+A661_ENTRY_VALID messages should be ignored if the value of the Enable parameter is anything 
+but A661_TRUE_WITH_VALIDATION.
+\<close>
+
+end

src/ontologies/ARINC661/CabineTemperature.thy

@@ -0,0 +1,30 @@
+theory CabineTemperature
+  imports ARINC_661
+
+begin
+
+value*[TemperatureCelciusScale::Picture, widget_ident=4642,parent_ident="Some 4641"]
+\<open>@{Picture \<open>TemperatureCelciusScale\<close>}\<close>
+value*[TemperatureIndicatedPointer::Symbol, widget_ident=4643,parent_ident="Some 4641"]
+\<open>@{Symbol \<open>TemperatureIndicatedPointer\<close>}\<close>
+value*[TemperatureSelectedPointer::Symbol, widget_ident=4644,parent_ident="Some 4641"]
+\<open>@{Symbol \<open>TemperatureSelectedPointer\<close>}\<close>
+value*[IndicatedTempDRO::Label, widget_ident=4645,parent_ident="Some 4641", label_string="\<open>24\<close>"]
+\<open>@{Label \<open>IndicatedTempDRO\<close>}\<close>
+value*[IndicatedUnitLabel::Label, widget_ident=4645,parent_ident="Some 4641", label_string="\<open>C\<close>"]
+\<open>@{Label \<open>IndicatedUnitLabel\<close>}\<close>
+value*[IncreaseSelectTemp::PicturePushButton, widget_ident=4646,parent_ident="Some 4641"]
+\<open>@{PicturePushButton \<open>IncreaseSelectTemp\<close>}\<close>
+value*[DecreaseSelectTemp::PicturePushButton, widget_ident=4647,parent_ident="Some 4641"]
+\<open>@{PicturePushButton \<open>DecreaseSelectTemp\<close>}\<close>
+
+value*[CabinTempPanel::Panel, widget_ident=4641]
+\<open>@{Panel \<open>CabinTempPanel\<close>}\<close>
+
+value*[Layer66::Layer, layer_id=66, widgets_tree="{CabinTempPanel, DecreaseSelectTemp, IncreaseSelectTemp, IndicatedUnitLabel, IndicatedTempDRO, TemperatureSelectedPointer, TemperatureIndicatedPointer, TemperatureCelciusScale}"]
+\<open>@{Layer \<open>Layer66\<close>}\<close>
+
+value*[CabineTemperature::Window, application_id="6788", contained_layers="{@{Layer \<open>Layer66\<close>}}"]
+\<open>@{Window \<open>CabineTemperature\<close>}\<close>
+
+end

src/ontologies/ARINC661/paper.thy

@@ -0,0 +1,156 @@
+(*<*)
+theory "paper"
+  imports "Isabelle_DOF.scholarly_paper"
+begin
+
+open_monitor*[this::article]
+
+declare[[ strict_monitor_checking  = false]]
+declare[[ Definition_default_class = "definition"]]
+declare[[ Lemma_default_class      = "lemma"]]
+declare[[ Theorem_default_class    = "theorem"]]
+
+define_shortcut*  isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
+                  isadof   \<rightleftharpoons> \<open>\isadof\<close>
+
+(*>*)
+
+(********************************************************)
+(* TITLE ************************************************)
+title*[tit::title]\<open>Formal Conformance of a Safety-Critical UI-Component with the ARINC Standard\<close>
+
+(**********************************************************)
+(* AUTHORS ************************************************)
+author*[idir,email="\<open>idir.aitsadoune@centralesupelec.fr\<close>",
+        affiliation="\<open>LMF, CentraleSupelec, Université Paris-Saclay\<close>"]
+\<open>Idir Ait-Sadoune\<close>
+author*[nicolas,email="\<open>nicolas.meric@lri.fr\<close>",affiliation="\<open>LMF, Université Paris-Saclay\<close>"]
+\<open>Nicolas Méric\<close>
+author*[bu,email= "\<open>wolff@lri.fr\<close>",affiliation = "\<open>LMF, Université Paris-Saclay\<close>"]
+\<open>Burkhart Wolff\<close>    
+
+(***********************************************************)
+(* ABSTRACT ************************************************)
+abstract*[abs, keywordlist="[\<open>w1\<close>,\<open>w2\<close>,\<open>w3\<close>,\<open>w4\<close>]"]
+\<open> We describe a new case-study in the domain of user-interfaces (UI) for safety-critical avionics systems.
+  We use \<^isadof> designed to handle documents with both formal and informal in order
+  to \<^emph>\<open>model\<close> the ontology of the relevant  ARINC 661 standard as well as the semi-formal 
+  \<^emph>\<open>description\<close> for a concrete UI component. The purpose of the exercise is to demonstrate
+  the conformance of the formal component model and its conformance to both the informal as
+  well as semi-formal, ontologically modeled aspects of the standard.
+  
+  In particular, We show how ontological invariants can be linked to safety-properties 
+  in the UI domain.
+\<close>
+text\<open>\<close>
+
+(***************************************************************)
+(* INTRODUCTION ************************************************)
+section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> Introduction \<close>
+text*[introtext::introduction]
+\<open>
+Our article should cover the following points:
+- Isa_Dof framework and its features to annotate informal texts with formal concepts of ontologies.
+- Checking the conformance of object instances with an ontology model in the context of ARINC 661 standard.
+- Possibility of expressing invariants (the case of the propagation of the visible and enable properties 
+between the root widget and the child widgets is to be treated)
+- modelling of the UA Validation process.
+\<close>
+
+(***************************************************************)
+(* BACKGROUND **************************************************)
+section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> Background \<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+subsection*[isabelle::technical,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> The Isabelle System  \<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+subsection*[isadof::technical,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> The Isa_DOF Framework  \<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+(***************************************************************)
+(* CASE STUDY **************************************************)
+section*[arinc::example,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> Case study : ARINC 661 and Multi-Purpose Interactive Application (MPIA)\<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+subsection*[arincmod::text_section]
+\<open> Modeling ARINC 661 in \<^isadof> \<close> 
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+subsection*[mpiamod::text_section]
+\<open> Checking MPIA conformance in \<^isadof> \<close> 
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+subsection*[gendoc::text_section]
+\<open> Document generation with \<^isadof> \<close> 
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+(***************************************************************)
+(* INVARIANTS **************************************************)
+section*[inv::technical,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> Expressing Invariants in ISADOF\<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+(***************************************************************)
+(* The UA Validation process. **********************************)
+section*[validation::technical,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> The User Application (UA) Validation process \<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+
+(*************************************************************)
+(* RELATED WORK ************************************************)
+section*[related::conclusion,main_author="Some(@{docitem ''bu''}::author)"]
+\<open>Related Work\<close>
+text
+\<open>
+bla bla bla bla ...
+\<close>
+
+(*************************************************************)
+(* CONCLUSION ************************************************)
+section*[conclusion::conclusion,main_author="Some(@{docitem ''bu''}::author)"]
+\<open>Conclusion\<close>
+text
+\<open>
+Conclusion content
+\<close>
+
+(*<*)
+
+close_monitor*[this]
+
+end
+(*>*)