MobiCa: Mobile Cloud Computing Language


Deciding whether to offload some computation is a crucial issue in mobile cloud computing systems. Various proposals in the literature try to face this problem taking decisions at design time, relying on the developer’s expectations or basing the choice on resource usage prediction. We propose a new methodology based on a formal framework, whose goal is to provide runtime support for offloading decisions. By means of a domain specific language (MobiCa), a developer can define both system and application structure, in terms of devices involved, computational power, code partitioning, required memory etc. Using a formal verification technique, based on the well-known model checker UPPAAL, the framework provides exhaustive and automatic decision support for offloading decisions. Using the resulting trace generated at runtime by UPPAAL, driven by some optimization query verified on the timed automata model associated with the MobiCa specification, the framework decides which fragments should be remotely executed. This process allows one to reduce memory and battery consumption, ensuring at the same time the best system performance.


Luca Aceto, Andrea Morichetta and Francesco Tiezzi. Decision Support for Mobile Cloud Computing Applications via Model Checking. Technical Report, IMT, 2014.


  • Stand-alone MCC compiler download
  • Eclipse plugin  link
  • Navigator MobiCa example download
  • Navigator UPPAAL example download (equipped with the verification queries)


  • Java
  • Eclipse


Stand-alone: Download in a target folder the MCC compiler and the MobiCa example. Unzip the MobiCa example and from the terminal move to the target folder and run the compiler.

java -jar MCC-compiler.jar navigator.mcc

The system will  create a src-gen forlder containing the Network.xml file directly editable from UPPAAL.

Eclipse plugin: Download an Eclipse IDE for Java Developers and install the plugin.

Help ->Install New Software -> Add

select MobiCa, click next and then finish.




click OK for security warning and then restart Eclipse.

For create a new MobiCa project  File -> New -> Project.







click Next

Insert the name and press Finish.

Right click on MCC project in the Package Explorer -> New -> File

Insert the file name with extension “.mcc” and press Finish.

Click yes for accept the MobiCa view and start to edit the navigator file according the MobiCa syntax.

Once completed the editing, save the file (Ctrl+s) and eclipse automatically generate the UPPAAL input file in:  MCC project -> src-gen -> “name of the system”.xml.

Open the generated .xml file with UPPAAL and perform some analysis.



A cost/reward method for optimal infinite scheduling in Mobile Cloud Computing

Luca Aceto, Kim G. Larsen, Andrea Morichetta, and Francesco Tiezzi



For suggestions, remarks, bugs or requests please do not hesitate to contact any of us.