Edit Star

`Name:`

Context-Sensitive Middleware-Based Software Applications `Domain:`

Algorithm`Functionality:`

The system includes two features:
(i) As far as possible, every visitor can personalize their favorite level of illumination irrespectively of their location within the zone.
(ii) At the same time, the system maximizes energy savings by dimming unnecessary streetlights. The system assumes that the effective distance for any streetlight to serve a visitor is at most 5 meters. And the testing is for the unit testing of the function $PowerUp()$ `Input:`

$s$ no. of surrounding streetlinghts of a visitor;
$l_f$ the favorite illumination(radiance) of the visitor;
$l_n$ the illumination(radiance) at the visitor site;
$p_v$ visitor's $(x,y)$ position;
$l_0$ the illumination(radiant intensity) emitted from the streetlight;
$p_l$ $(x,y)$ position of the steetlight;
$r_{eff}$ is the radius of the effective illumination region of a streetlight;
$r^2(p_i,p_0)$ is a function to return the square of the distance between the streetlight at position $p_0$ and the visitor at position $p_i$;
$l_{f_1}$ and $l_{f_2}$ are the favorite illuminations of the visitor at positions $p_1$ and $p_2$;
The symbol ''$\approx$'' denotes that the two values are approximately equal within an application-specific tolerance limit of $2\varepsilon $;
`Output:`

$$l_n=\sum_{i=1}^s \frac{l_{0}^{(i)}}{d^{(i)}}$$
where $l_0^{(i)}$ and $d^{(i)}$ denote the context variable $l_0$ and the derived context $d$,respectively, from the $i$th surrounding streetlight.And $d=(p_l\cdot x-p_v\cdot x)^2 + (p_l\cdot y-p_v\cdot y)^2$ is the distance between the streetlight and the visitor.
Testing Context-Sensitive Middleware-Based Software Applications https://doi.org/10.1109/CMPSAC.2004.1342879

`Description:`

`Property:`

$MR_{PowerUp}=\{(p_1,p_2,l_{n_1},l_{n_2},l_{f_1},l_{f_2},p_0,r_{eff}) \mid r^2(p_1,p_0) \leq r^2_{eff} \wedge r^2(p_2,p_0) \leq r^2_{eff} \wedge l_{f_1}=l_{f_2} \Rightarrow l_{n_1} \approx l_{n_2}$ `Source input:`

$(p_0,p_1,l_{f_1},r_{eff})$ `Source output:`

$l_{n_1}$ `Follow-up input:`

$(p_0,p_2,l_{f_2},r_{eff})$ `Follow-up output:`

$l_{n_2}$ `Input relation:`

$r^2(p_1,p_0) \leq r^2_{eff} \wedge r^2(p_2,p_0) \leq r^2_{eff} \wedge l_{f_1}=l_{f_2}$ `Output relation:`

$l_{n_1} \approx l_{n_2}$ `Pattern:`