Artifact Content
Not logged in

Artifact 27c71502aebd876e2b331446f1e1401adf8415a0:

Wiki page [Experiment: mmmv_silkexec: spec Ideas 01] by martin_vahi on 2017-05-30 15:25:54.
D 2017-05-30T15:25:54.340
L Experiment:\smmmv_silkexec:\sspec\sIdeas\s01
P 7b453ae2f53fce55ab0bf5477771664fbb685829
U martin_vahi
W 1558
<p>This page is for a semi-random collection of ideas, how to
improve/change/create the specification of the
<a href="./wiki?name=Experiment:+mmmv_silkexec">mmmv_silkexec</a>.</p>

<p><br>
</p>

<h1>General Observations</h1>

<p>Due to the fact that applications work as a combination of application
specific code and the dependencies of the application, in some cases some code
is loaded dynamically, at runtime, a <b>proper formal verification task gets
prohibitively large pretty quickly</b>. Even, if formal verification were
possible, the <b>behavior of software packages can depend on hardware</b>,
which varies between different users. If hardware is guaranteed to be the same
for all users, for example, if all users use a specific version of the
Raspberry Pi, then the fact that <b>compile-time parameters depend on the
previously installed packages can be countered by installing all packages of
the package collection in the exact order that they were compiled and tested at
test server</b>, but even then the test server at least partly relies on the
tests that have been supplied with the software package, by the software
package creator, which may be a different person than the author of the
packaged software. It is possible for the software packager to accompany the
upstream deliverables with its own, additional, tests.</p>

<p><br>
</p>

<h1>Hardware Related Observations</h1>

<p></p>
<ul>
<li><br>
</li>
</ul>

<p></p>

<p><br>
</p>

<h1>Social Aspects Related Observations</h1>

<p><br>
</p>

<p><br>
</p>

<p><br>
</p>

<p><br>
</p>

Z 479de07f8c7801b8eae4c2cd9ef186aa