The basics of Alvis language have been worked out in the NCN research project Formal methodology of real-time systems development with the use of visual object process algebra (Formalna metodyka realizacji systemów czasu rzeczywistego z wykorzystaniem wizualnej obiektowej algebry procesów) founded by National Science Centre in Poland.

• Marcin Szpyrka, Prof. - project leader mszpyrka [at] agh [dot] edu [dot] pl
• Tomasz Szmuc, Prof tsz [at] agh [dot] edu [dot] pl
• Rafał Mrówka, PhD Rafal [dot] Mrowka [at] agh [dot] edu [dot] pl
• Piotr Matyasik, PhD ptm [at] agh [dot] edu [dot] pl
• Leszek Kotulski, Prof. kotulski [at] agh [dot] edu [dot] pl
• Jarosław Baniewicz, MSc jarek.baniewicz [at] gmail [dot] com
• Krzysztof Balicki, MSc kbalicki [at] univ [dot] rzeszow [dot] pl
• Wojciech Witalec, MSc witwojtek [at] gmail [dot] com
• Adam Sędziwy, PhD sedziwy [at] agh [dot] edu [dot] pl

Alvis modelling language, communication diagrams, Haskell, XCCS process algebra, hierarchical modelling, embedded systems, visual design, formal verification

The aim of the Alvis research project was to work out a new language for embedded systems modelling and verification. The language also called Alvis has been defined as a kind of a happy medium between formal and practical modelling languages. It combines possibilities of formal models verification with flexibility and simplicity of practical programming languages.

Alvis is a successor of the XCCS modelling language, which is an extension of the CCS process algebra. However, instead of algebraic equations, Alvis uses a high level programming language based on the Haskell syntax. Alvis combines hierarchical graphical modelling with high level programming language. A model consists of three layers. The graphical layer is used to define data and control flow among agents. The code layer is used to describe behaviour of individual agents. The third system layer is used for simulation and analysis purposes.

Together with the modelling language, the Alvis team is developping the Alvis Toolkit i.e. software for the design and verification of Alvis models.

• ATMEL AVR microprocessor,
• RTLinux operating system,
• C and C++ programming languages,
• Haskell programming language.

• 22.09.2011 ADM2011 Conference Marcin Szpyrka has presented paper entitled Formal verification of embedded systems using the Alvis approach.
• 21.09.2011 ADM2011 Conference Leszek Kotulski has presented paper entitled Solving large-scale multipoint lighting design problem using multi-agent environment.
• 13.09.2011 KES 2011 Conference Leszek Kotulski has presented paper entitled Snapshot reachability graphs for Alvis model.
• 13.09.2011 KES 2011 Conference Leszek Kotulski has presented paper entitled Labelled Transition System generation from Alvis language.
• 13.09.2011 SCR 2011 Conference Piotr Matyasik has presented paper entitled Specyfikacja otoczenia systemów wbudowanych modelowanych w języku Alvis.
• 13.09.2011 SCR 2011 Conference Jarosław Baniewicz has presented paper entitled Detekcja zakleszczenia w systemie ABS z zastosowaniem języka Alvis.
• 20.07.2011 Worldcomp 2011 Conference Marcin Szpyrka has presented paper entitled Specification of embedded systems environment behaviour with Alvis modelling language.
• 20.07.2011 Worldcomp 2011 Conference Leszek Kotulski has presented paper entitled Graph representation of hierarchical Alvis model structure.
• 17.06.2011 MIXDES 2011 Conference Rafał Mrówka has presented paper entitled Modelling of Signals Handling with Alvis. The Outstanding Paper Award has been presented to authors for the paper.
• 17.06.2011 MIXDES 2011 Conference Jarosław Baniewicz has presented paper entitled Priority inversion detection in Alvis models.
• .06.2011 ECMS 2011 Conference Piotr Matyasik has presented paper entitled Practical approach to modelling and verification of concurrent systems with Alvis.
• 09.06.2011 KNWS 2011 Conference Marcin Szpyrka has presented paper entitled Introduction to Alvis modelling language.
• 15.05.2011 Icannga 2011 Conference Leszek Kotulski has presented paper entitled Parallel Graph Transformations Supported by Replicated Complementary Graphs
• 12.05.2011 Explicite Seminar - Jarosław Baniewicz has given a lecture on Formal verification of Alvis models
• 24.03.2011 Explicite Seminar - Marcin Szpyrka has given a lecture entitled Introduction to Alvis on the current state of the Alvis project.
• 20.01.2011 Explicite Seminar - Wojciech Witalec has given a lecture on Introduction to temporal logic and model checking.
• 16.12.2010 Delphi Seminars for AGH-UST - Jarosław Baniewicz has given a lecture on Process algebra. Car alarm simulation.
• 09.12.2010 Explicite Seminar - Jarosław Baniewicz has given a lecture on Process algebras – historical perspective and current applications.
• 28.09.2010 SCR 2010 Conference Marcin Szpyrka has presented paper entitled Modelling embedded systems with Alvis.
• 25.06.2010 MIXDES 2010 Conference Piotr Matyasik has presented paper entitled Alvis Approach to Hexor Robot Controller Development.
• 19.05.2010 Seminar at UR - Krzysztof Balicki has given lecture on Tag Abstraction for XCCS Modelling Language.
• 12.05.2010 Seminar at UR - Krzysztof Balicki has given lecture on XCCS Modelling Language.
• 05.05.2010 Seminar at UR - Krzysztof Balicki has given lecture on CCS Process Algebra.
• 15.02.2010 Polish-German Seminar at AGH - Marcin Szpyrka has given lecture on Alvis - modelling language for embedded systems.
• 03.12.2009 Explicite Seminar - Zbigniew Grzybek and Marcin Szpyrka has given a lecture on Verification of XCCS models with CADP toolbox, more...
• 26-27.11.2009 7th Conference on Computer Methods and Systems CMS'09, Krakow, Poland - Marcin Szpyrka has presented paper entitled Haskell approach to rule-based systems analysis.
• 12-14.10.2009 4rd IFIP TC2 Central and East European Conference on Software Engineering Techniques, Krakow, Poland CEE-SET 2009 - Piotr Matyasik has presented paper entitled Modelling Hexor Robot Behaviour with Value Passing XCCS.
• 28-30.09.2009 Workshop on Concurrency, Specification, and Programming CS&P 2009 - Krzysztof Balicki has presented paper entitled Tags Abstraction for XCCS Modelling Language.
• 14.04.2009 Alvis project starts (official date).
• 04.02.2009 Alvis project presented at Explicite Seminar more...

@Article{Szp:etal:PAK:11,
author =   {Szpyrka, M. and Matyasik, P. and Mr\'owka, R. and Witalec, W. and Baniewicz, J. and Balicki, K.},
title =    {Introduction to {A}lvis modelling language},
journal = {Measurement Automation and Monitoring (PAK)},
year = {2011},
volume = {57},
number = {9},
pages = {1086-1089}
}

@Article{Szp:PAR:11,
author =   {Szpyrka, M.},
title =    {Modelling concurent systems with {A}lvis},
journal = {Pomiary Automatyka Robotyka},
year = {2011},
volume = {15},
number = {12},
pages = {239-240}
}

@Article{KoSzp:11:ADM,
author = {Kotulski, L. and Szpyrka, M.},
title = {Formal Verification of Embedded Systems Using the {A}lvis Approach},
journal = {Key Engineering Materials},
year = {2011},
volume = {486},
pages = {209-212}
}

@Article{SedzKo:11:ADM,
author = {Sędziwy, A. and Kotulski, L.},
title = {Solving large-scale multipoint lighting design problem using multi-agent environment},
journal = {Key Engineering Materials},
year = {2011},
volume = {486},
pages = {197-182}
}

@InCollection{KoSedz11:LNCS:ICANNGA,
author = {Kotulski, L. and Sędziwy, A.},
title = {Parallel graph transformations supported by replicated complementary graphs},
booktitle = {Adaptive and natural computing algorithms -- ICANNGA 2011},
year = {2011},
pages = {254-264},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {6594},
address = {Berlin, Heidelberg},
editor = {Dobnikar, A. and Lotri\v{c}, U. and Ster, B.},
} 


@InCollection{SzpMatMr11:Springer,
author = {Szpyrka, M. and Matyasik, P. and Mrówka, R.},
title = {Alvis -- modelling language for concurrent systems},
publisher = {Springer-Verlag},
year = {2011},
series = {SCI},
booktitle = {Intelligent Decision Systems in Large-Scale Distributed Environments},
editor = {Bouvry, P. and Gonzalez-Velez, H. and Kołodziej, J.},
volume = {362},
pages = {315--342}
}

@InProceedings{SzpMatMr11:ECMS:Krakow,
author = {Szpyrka, M. and Matyasik, P. and Mrówka, R.},
title = {Practical approach to modelling and verification of concurrent systems with {A}lvis},
address = {Krakow, Poland},
year = {2011},
booktitle = {Proc. of the 25th European Conference on Modelling and Simulation},
pages = {539-545}
}

@InProceedings{BanSzp:11:Mixdes:priorityinversion,
author =   {Baniewicz, J. and Szpyrka, M.},
title =    {Priority inversion detection in {A}lvis models},
booktitle = {Proc. of Mixdes 2011, the 18th International Conference Mixed Design of Integrated Circuits and Systems},
year = {2011},
month = {June 16-18},
address = {Gliwice, Poland},
pages =  {638-643}
}

@InProceedings{Szp_atal:11:Mixdes:signalshandling,
author =   {Szpyrka, M. and Matyasik, P. and Mrówka, R. and Kotulski, L.},
title =    {Modelling of signals handling with {A}lvis},
booktitle = {Proc. of Mixdes 2011, the 18th International Conference Mixed Design of Integrated Circuits and Systems},
year = {2011},
month = {June 16-18},
address = {Gliwice, Poland},
pages =  {627-631}
}


@InCollection{SzpKo11:LNCS:SRgraphs,
author = {Szpyrka, M. and Kotulski, L.},
title = {Snapshot reachability graphs for {A}lvis models},
booktitle = {Knowledge-Based and Intelligent Information and Engineering Systems -- KES 2011},
year = {2011},
pages = {190-199},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {6881},
address = {Berlin, Heidelberg},
editor = {K\"{o}nig, A. and Dengel, A. and Hinkelmann, K. and Kise, K. and Howlett, R.J. and Jain, L.C. },
} 

@InCollection{KoSzpSedz11:LNCS:LTSgeneration,
author = {Kotulski, L. and Szpyrka, M. and S\k{e}dziwy, A.},
title = {Labelled Transition System Generation from {A}lvis Language},
booktitle = {Knowledge-Based and Intelligent Information and Engineering Systems -- KES 2011},
year = {2011},
pages = {180-189},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {6881},
address = {Berlin, Heidelberg},
editor = {K\"{o}nig, A. and Dengel, A. and Hinkelmann, K. and Kise, K. and Howlett, R.J. and Jain, L.C. },
} 

@Article{Szp_atal:11:Automatyka,
author = {Szpyrka, M. and Matyasik, P. and Mr\'owka, R. and Witalec, W. and Baniewicz, J. and Kotulski, L.}, 
title = {Introduction to modelling embedded systems with {A}lvis},
journal = {Automatyka},
year = {2011},
volume = {15},
number = {2},
pages = {435-442}
}

@InProceedings{Szp_atal:11:KNWS,
author =   {Szpyrka, M. and Matyasik, P. and Mr\'owka, R. and Witalec, W. and Baniewicz, J. and Balicki, K.},
title =    {Introduction to {A}lvis modelling language},
booktitle = {KNWS'11: Materiały 8. konferencji naukowej ,,Informatyka – sztuka czy rzemiosło''},
year = {2011},
month = {7-10 czerwca},
address = {Karpacz},
pages =  {185-190}
}

@InCollection{BanSzp:11:SCR:zakleszczenieABS,
author = {Baniewicz, J. and Szpyrka, M.},
title = {Detekcja zakleszczenia w systemie {ABS} z~zastosowaniem języka {A}lvis},
booktitle = {Projektowanie, analiza i implementacja systemów czasu rzeczywistego},
year = {2011},
pages = {77-86},
publisher = {Wydawnictwa Komunikacji i Łączności},
address = {Warszawa},
editor = {Trybus, L. and Samolej, S.},
} 

@InCollection{SzpMaMr:11:SCR:otoczenie,
author = {Szpyrka, M. and Matyasik, P. and Mrówka, R.},
title = {Specyfikacja otoczenia systemów wbudowanych modelowanych w języku {A}lvis},
booktitle = {Projektowanie, analiza i implementacja systemów czasu rzeczywistego},
year = {2011},
pages = {65-75},
publisher = {Wydawnictwa Komunikacji i Łączności},
address = {Warszawa},
editor = {Trybus, L. and Samolej, S.},
} 


@InProceedings{SzpKoMa:11:Worldcomp,
booktitle = {Proc. of the 2011 International Conference on Embedded Systems and Applications ESA'11 (part of Worldcomp 2011)},
author = {Szpyrka, M. and Kotulski, L. and Matyasik, P.},
year = {2011},
title = {{Specification of embedded systems environment behaviour with {A}lvis modelling language}},
address = {Las Vegas, Nevada, USA},
month = {July 18-21},
}

@InProceedings{KoSzp:11:Worldcomp,
booktitle = {Proc. of the 2011 International Conference on Foundations of Computer Science FCS'11 (part of Worldcomp 2011)},
author = {Kotulski, L. and Szpyrka, M.},
year = {2011},
title = {{Graph representation of hierarchical {A}lvis model structure}},
address = {Las Vegas, Nevada, USA},
pages = {95-101},
month = {July 18-21},
}

@InProceedings{KoSedz:11:DEPCOS,
booktitle = {Problems of Dependability and Modelling},
author = {Kotulski, L. and Sędziwy, A.},
year = {2011},
title = {Inter-Agent Communication Protocol Supporting Distributed Graph Transformations},
pages = {127-142},
publisher = {Oficyna Wydawnicza Politechniki Wrocławskiej},
}

@incollection{SzpMatMr10:SCR,
author = {Szpyrka, M. and Matyasik, P. and Mr\'owka, R.},
title = {Modelowanie systemów wbudowanych w języku {A}lvis},
booktitle = {Metody wytwarzania i zastosowania systemów czasu rzeczywistego},
editor = {Trybus, L. and Samolej, S.},
publisher = {Wydawnictwa Komunikacji i Łączności},
pages = {25-35},
year = {2010}
}

@InProceedings{SzpMatMr:10:Mixdes:HexorAlvis,
author =   {Szpyrka, M. and Matyasik, P. and Mrówka, R.},
title =    {Alvis approach to {H}exor robot controller development},
booktitle = {Proc. of Mixdes 2011, the 17th International Conference Mixed Design of Integrated Circuits and Systems},
year = {2010},
month = {June 24-26},
address = {Wrocław, Poland},
pages =  {595-600}
}

@Article{SzpMatMr:10:Elektronika:HexorAlvis,
author =   {Szpyrka, M. and Matyasik, P. and Mrówka, R.},
title =    {Alvis approach to {H}exor robot controller development},
journal = {Elektronika},
year = {2010},
volume = {11},
pages = {63-66}
}

@InProceedings{Szp09:CMS:RBSHaskell,
author = {Szpyrka, M.},
title = {Haskell approach to rule-based systems analysis},
address = {Krakow, Poland},
year = {2009},
booktitle = {Proc. of the 7th International Conference Computer Methods and Systems (CMS 2009)},
pages = {111-116}
}

@InProceedings{BaSzp09:CSP,
author = {Balicki, K. and Szpyrka, M.},
title = {Tag abstraction for XCCS modelling language},
booktitle = {Proceedings of the Concurrency Specification and Programming Workshop (CSP 2009)},
year = {2009},
pages = {26-37},
month = {September 28-30},
address = {Krakow, Poland},
volume = {1}
} 

@Article{BalSzp09-FI,
author = {Balicki, K. and Szpyrka, M.},
title = {Formal Definition of {XCCS} Modelling Language},
journal = {Fundamenta Informaticae},
year = {2009},
volume = {93},
number = {1-3},
pages = {1-15}
}

@InCollection{SzpMa09-CEESET,
author = {Szpyrka, M. and Matyasik, P.},
editor = {Huzar, Z. and Nawrocki, J. and Szpyrka, M.},
title = {Modelling {H}exor robot behaviour with value passing {XCCS}},
booktitle = {Software Engineering Techniques in Progress (the 4th IFIP TC2 Central and East European Conference on Software Engineering Techniques, CEE-SET 2009)},
publisher = {AGH University of Science and Technology Press},
year = {2009},
address = {Krakow, Poland},
pages = {67-78}
}