logseq/pages/PAPERS___DSL-FOR-IOT-TESTING.md

type:: JOURNAL date:: 22-11-2023 - 12:14 full-title:: external-links:: davidediruscio/MAUDE (github.com) First logic programming languages - Google Docs todoist:: Todoist https://docs.google.com/document/d/1pkhzeeFYvXgsf4kXLdn03BwX-EkgsQI3IVFU6Eovji0/edit?usp=sharing year:: 2024 date-start:: 22-11-2023 status:: DOING venue:: priority:: P1 leader:: progress:: {{renderer : todomaster}}

- ## Meeting del [[06-06-2025]]
  type:: [[meeting]]
	- Si e' deciso di andare per IST
		- 49 vs 85 linee di codici
	- Pensare a come valutare la convenienza dell'uso del linguaggio.
		-
- ## NOTES
	- Aapproach to detect possible faults that can occur when giving a time series to an input port of an IoT component and get output data from the corresponding output. The kinds of faults that we have carrently identified are the following:
		- EARLY: output is provided too early
		- LATE: output is provided too late
		- VALUE COARSE: output values are out of the expected range
		- VALUE SUBTLE:
		- OMISSION: no output is generated
		- COMMISSION: output is generated when it is not expected
	- In particular, the approach that we want to develop relies on the following basic concepts:
		- Failure types (currently defined as above)
		- Time series: they represent streams of values that are given as input to input ports.
		- Time series operators: Given a time series, we want to support the specification of
			- Addition of elements
			- Removal of elements
			- Changes of existing elements
	- Thus the approach should support the specification of:
		- Input time series
		- Mutations of the input
		- Check if some faults is detected to the time series in output for some of the mutations given in input
	- Both mutations and checks are fault specific. Thus, for each fault we need to specify mutations that make sense, and specify properties that if violated means that the corresponding faults occurred.
	- Said that, I would like to formulate the approach in MAUDE. I alread defined the following module:
		- mod TIME-SERIES-MODULE is
		    protecting INT .  --- Importing predefined sort for integers
		  --- Defining sorts
		    sort TimeStamp Series .
		  --- Defining constructors
		    op empty : -> Series .
		    --- The pair consists of TIME @ VALUE
		    op _@_ : Int Int -> TimeStamp [ctor] .
		    op _;_ : TimeStamp Series -> Series [ctor] .
		  --- Operations to mutate, insert and delete a value at a given time
		    op mutateAt : Int Int Series -> Series .
		    op insertAt : Int Int Series -> Series .
		    --- op insertRandomAt : Int Series -> Series .
		    op deleteAt : Int Series -> Series .
		    --- Variables for the equations
		    var T V T' V' : Int .
		    var S : Series .
		  --- Equations for mutateAt
		    ceq mutateAt(V', T, T @ V ; S) = T @ V' ; S if true .
		    ceq mutateAt(V', T', T @ V ; S) = T @ V ; mutateAt(V', T', S) if T =/= T' .
		    eq mutateAt(V', T', empty) = empty .
		  --- Equations for insertRandomAt
		    --- eq insertRandomAt(T, empty) = T @ (loop m "python random.py") ; empty .
		  --- Equations for insertAt
		    eq insertAt(V, T, empty) = V @ T ; empty .
		    ceq insertAt(V, T, T' @ V' ; S) = T @ V ; T' @ V' ; S if T <= T' .
		    ceq insertAt(V, T, T' @ V' ; S) = T' @ V' ; insertAt(V, T, S) if T > T' .
		  --- Equations for deleteAt
		    eq deleteAt(T, empty) = empty .
		    ceq deleteAt(T, T @ V' ; S) = S if true .
		    ceq deleteAt(T, T' @ V' ; S) = T' @ V' ; deleteAt(T, S) if T =/= T' .
		  endm
	- Can you help complete the module to completely support the approach as described before?
	- Adesso, non ho ancora gli elementi per capire:
	  
	  1) quanto abbia senso definire il DSL
	  2) collegato al punto precedente, quanto e' conveniente avere MAUDE nel "loop"
	  
	  tralasciando per un attimo 2) non riusciamo a dare ancora evidenza che il linguaggio in 1) sia necessario. Mi riferisco al potere espressivo del DSL e se invece e' necessario avere un linguaggio general purpose considerando il fatto che potrei volere definire:
		- fault types a piacere
		- mutazioni a piacere
- ## MEETINGS
- ## READINGS
	- [[MAUDE-Manual]]
- ## TASKs
- ## QUESTIONS TO ANSWER
  {{query (and [[question]][[PAPERS/DSL-FOR-IOT-TESTING]])}}
- ## [[PAPERS/NOTES]]
	- MAUDE sembra essere un buon candidato come linguaggio target per dare semantica al DSL in fase di definizione.
	- Come descritto [1 Introduction (uma.es)](https://maude.lcc.uma.es/maude321-manual-html/maude-manualch1.html#x4-140001.2)
		- In the context of Maude, such property specifications can be given in a variety of ways:
			- as nonexecutable equations, memberships, and rules in Maude’s native logics;
			- as first-order logic formulas; or
			- as invariants or, more generally, linear temporal logic formulas.
		- Experience has shown that this makes rewriting logic a very expressive *semantic framework* for system specification. Here we only mention some relevant areas:
			- *Models of computation*. Many models of computation, including a very wide range of concurrency models, can be naturally specified as different theories within rewriting logic, and can be executed and analyzed in Maude.
			- ==*Programming languages*==. Rewriting logic has very good properties—combining in a sense the best features of denotational semantics’ equational definitions with the strengths of structural operational semantics—to give formal semantics to a programming language. Furthermore, in Maude such semantics definitions become the basis of interpreters, model checkers, and other program analysis tools for the language in question.
			  background-color:: yellow
			- *Distributed algorithms and systems*. Because of its good features for concurrent, object-based specification, many distributed algorithms and systems, including, for example, network protocols and cryptographic protocols, can be easily specified and analyzed in Maude. Furthermore, making use of Maude’s external object facility to program interactions with internet sockets, one can not just specify but also program various distributed applications in a declarative way (see Section [9](https://maude.lcc.uma.es/maude321-manual-html/maude-manualch9.html#x61-1320009)).
			- *Biological systems*. Cell dynamics is intrinsically concurrent, since many different biochemical reactions happen concurrently in a cell. By modeling such biochemical reactions with rewrite rules, one can develop useful symbolic mathematical models of cell biology. Such models can then be used to study and predict biological phenomena.